Abstract. Local search is widely used for solving the propositional satisfiability problem. Papadimitriou [Pap91] showed that randomized local search solves 2-SAT in polynomial time. Recently, Schöning [Sch99] proved that a close algorithm for k-SAT takes time (2-2/k)ⁿ up to a polynomial factor. This is the best known worst-case upper bound for randomized 3-SAT algorithms.

We describe a deterministic local search algorithm for k-SAT running in time (2-2/(k+1))ⁿ up to a polynomial factor. The key point of our algorithm is the use of covering codes instead of random choice of initial assignments. Compared to other "weakly exponential" algorithms, our algorithm is technically quite simple. We also describe an improved version of local search. For 3-SAT the improved algorithm runs in time 1.481ⁿ up to a polynomial factor. Our bounds are better than all previous bounds for deterministic k-SAT algorithms.

[ Full text (journal submission): .ps.gz ]