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 (20.5625 n) …

We propose and analyze a simple new randomized algorithm, called ResolveSat, for nding
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. We show that, for each k, the running
time of ResolveSat on ak {CNF formula is signi cantly better than 2n, even in the worst case …