Proceedings of ICALP'00, LNCS 1853, Springer-Verlag, 2000.

**Abstract.**
We show that satisfiability of formulas in k-CNF can be
decided deterministically in time close to (2k/(k+1))^{n}, where n is
the number of variables in the input formula. This is the best known
worst-case upper bound for deterministic k-SAT algorithms. Our algorithm
can be viewed as a derandomized version of Schöning's probabilistic
algorithm presented at FOCS'99. The key point of our algorithm
is the use of covering codes together with local search. Compared to
other "weakly exponential" algorithms, our algorithm is technically
quite simple.

We also show how to improve the bound above by moderate technical effort.
For 3-SAT the improved bound is 1.481^{n}.

[ Full text: .ps.gz ((c) Springer-Verlag) ]

Back to the list of papers