An improved exponential-time algorithm for k-SAT

We propose and analyze a simple new randomized algorithm, called ResolveSat, for finding satisfying assignments of Boolean formulas in conjunctive normal form. The algorithm consists of two stages: a preprocessing stage in which resolution is applied to enlarge the set of clauses of the formula, followed by a search stage that uses a simple randomized greedy procedure to look for a satisfying assignment. Currently, this is the fastest known probabilistic algorithm for k-CNF satisfiability for k >= 4 (with a running time of O (2(0.5625n)) for 4-CNF). In addition, it is the fastest known probabilistic algorithm for k-CNF, k >= 3, that have at most one satisfying assignment (unique k-SAT) (with a running time O(2((2 ln 2-1)n+o(n))) = O(2(0.386...n)) in the case of 3-CNF). The analysis of the algorithm also gives an upper bound on the number of the codewords of a code defined by a k-CNF. This is applied to prove a lower bounds on depth 3 circuits accepting codes with nonconstant distance. In particular we prove a lower bound Omega(2(1.282...root n)) for an explicitly given Boolean function of n variables. This is the first such lower bound that is asymptotically bigger than 2(root n+o(root n)).