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.481n.
[ Full text: .ps.gz ((c) Springer-Verlag) ]