Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Paper:

TR05-102 | 13th September 2005 00:00

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

RSS-Feed




TR05-102
Authors: Evgeny Dantsin, Edward Hirsch, Alexander Wolpert
Publication: 20th September 2005 15:19
Downloads: 3316
Keywords: 


Abstract:

We give a deterministic algorithm for testing satisfiability of 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 [Dantsin and Wolpert, SAT 2005]. In comparison with the randomized algorithm in [Dantsin and Wolpert, SAT 2005], our deterministic algorithm is simpler and more intuitive.



ISSN 1433-8092 | Imprint