An improved exponential-time algorithm for <i>k</i> -SAT

TLDR

The authors introduce ResolveSat, a new randomized algorithm for finding satisfying assignments of k‑CNF formulas. ResolveSat first applies resolution to expand the clause set, then uses a randomized greedy search to locate a satisfying assignment, and its analysis also bounds the number of codewords of a k‑CNF code. ResolveSat achieves the fastest known probabilistic runtime for k‑CNF with k≥4 (O(2^0.5625 n)) and for unique k‑SAT with k≥3 (O(2^0.386 n)), and the analysis yields an asymptotically larger lower bound Ω(2^1.282 √n) for a specific Boolean function.

Abstract

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.5625 n ) 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 Ω(2 1.282…√&gt;i&lt;n&gt;/i&lt; ) for an explicitly given Boolean function of n variables. This is the first such lower bound that is asymptotically bigger than 2 √&gt;i&lt;n&gt;/i&lt; + o (√&gt;i&lt;n&gt;/i&lt;) .