Theoretical Computer Science 289/1, 2002, pp. 69-83.

**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)^{n} 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))^{n} 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^{n} up to a polynomial factor.
Our bounds are better than all previous bounds for deterministic
k-SAT algorithms.

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

Back to the list of papers