A deterministic (2-2/(k+1))n algorithm for k-SAT based on local search

Local search is widely used for solving the propositional satisfiability problem. Papadimitriou (1991) showed that randomized local search solves 2-SAT in polynomial time. Recently, Schoning (1999) 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 fir randomized 3-SAT algorithms (cf. also recent preprint by Schuler et al.). 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. (C) 2002 Elsevier Science B.V. All rights reserved.