Improved exponential-time algorithm for k-SAT

An algorithm, ResolveSat, a randomized variant of Davis, Longeman and Loveland (DLL) or Davis-Putnam procedure, for finding satisfying assignments of Boolean formulae in conjunctive normal form is presented. Rather than applying the DLL procedure to the input formula F, ResolveSat enlarges F by adding additional clauses using limited resolution before performing DLL. The basic idea behind the analysis is the same: a critical clause for a variable at a satisfying assignment gives rise to a unit clause in the DLL procedure with sufficiently high probability, thus increasing the probability of finding a satisfying assignment. The effect of multiple critical clauses in producing unit clauses is examined.