@inproceedings{57bafdbcc2884f328ac495ae212829f4,
title = "Clause shortening combined with pruning yields a new upper bound for deterministic SAT algorithms",
abstract = "We give a deterministic algorithm for testing satisfiability of Boolean formulas in conjunctive normal form with no restriction on clause length. Its upper bound on the worst-case running time matches the best known upper bound for randomized satisfiability-testing algorithms [6]. In comparison with the randomized algorithm in [6], our deterministic algorithm is simpler and more intuitive.",
author = "Evgeny Dantsin and Hirsch, {Edward A.} and Alexander Wolpert",
year = "2006",
doi = "10.1007/11758471_9",
language = "אנגלית",
isbn = "354034375X",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "60--68",
booktitle = "Algorithms and Complexity - 6th Italian Conference, CIAC 2006, Proceedings",
note = "6th Italian Conference on Algorithms and Complexity, CIAC 2006 ; Conference date: 29-05-2006 Through 31-05-2006",
}