Improved Exponential Algorithms for SAT and ClSP
Timon Hertli · Repository for Publications and Research Data (ETH Zurich) · 2015
Satisfiability of Boolean formulas (SAT) is one of the most prominent NP-complete problems.We consider k-SAT, the decision problem that asks whether formulas in conjunctive normal form (CNF) with clauses of size at most k are satisfiable, and the more general problem called (d, k)-ClSP (clause satisfaction problem) where the variables are d-valued instead of Boolean.For k-SAT and (d, k)-ClSP many algorithms have been presented whose running time is "moderately exponential" in the number of variables of the input formula.One of the fastest randomized algorithm for k-SAT is the PPSZ algorithm by Paturi, Pudlák, Saks, and Zane (FOCS 1998).We re-analyze the PPSZ algorithm and show that the bounds shown in the case where the input formula has at most one satisfying assignment (Unique k-SAT) hold in general, which was previously only known for k ≥ 5.We also show how to generalize PPSZ to (d, k)-ClSP, improving on the previous algorithms for most considered values of (d, k).Furthermore, we present a new algorithm based on PPSZ with exponentially better bounds for 3-SAT.For general k we show that in order to improve on PPSZ for k-SAT, it is enough to improve on PPSZ for Unique k-SAT.v