Clause Shortening Combined with Pruning Yields a New Upper Bound for Deterministic SAT Algorithms

摘要

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. In comparison with the randomized algorithm in [6], our deterministic algorithm is simpler and more intuitive.