Petersburg Department of Steklov Institute of Mathematics

PREPRINT 1/2000

ALGORITHMS FOR $k$-SAT BASED ON COVERING CODES

This preprint was accepted January 12, 2000
Contact: E.Dantsin E.Hirsch

ABSTRACT:
We show that for any $k$ and $\epsilon$, satisfiability of 
propositional formulas in $k$-CNF can be checked by a deterministic
algorithm running in time $poly(n) (2k/(k+1) + \epsilon)^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\"oning's
recent algorithm (FOCS'99) whose bound $poly(n) (2(k-1)/k)^n$ is the
best known bound for probabilistic 3-SAT algorithms. The key point of
our derandomization is the use of covering codes.

Like Sch\"oning's algorithm, our algorithm is quite simple. We show 
how to obtain slightly improved bounds by using a more thorough 
(but a more intricate) version of the algorithm. For example, for 
3-SAT the modified algorithm gives the bound $poly(n) 1.490^n$.