Clause Shortening Combined with Pruning Yields a New Upper Bound for Deterministic SAT Algorithms
Evgeny Dantsin, Edward Alekseevich Hirsch, Alexander Wolpert · 2005
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.