Source-linked AI summary
3-SAT Faster and Simpler - Unique-SAT Bounds for PPSZ Hold in General
Timon Hertli
TL;DR
For 3-SAT, the best general bound, O(1.32065^n), remained slower than Unique 3-SAT’s O(1.30704^n). The paper modifies PPSZ and assigns each satisfiable formula a cost that decreases during each algorithm step. O(1.30704^n) for 3-SAT improves on O(1.32065^n), and O(1.46899^n) for 4-SAT improves on O(1.46928^n).
Problem
For 3-SAT, the best general bound, O(1.32065^n), remained slower than Unique 3-SAT’s O(1.30704^n).
Source: §1 · p. 1Method
The paper modifies PPSZ and assigns each satisfiable formula a cost that decreases during each algorithm step.
Source: §1.1 · p. 2, §2 · p. 4Results
O(1.30704^n) for 3-SAT improves on O(1.32065^n), and O(1.46899^n) for 4-SAT improves on O(1.46928^n).
Source: §1.1 · p. 2Takeaways & Limitations
For k≥5, the analysis provides an alternative proof of the general k-SAT bound, while whether Unique-SAT and general k-SAT bounds match in general remains open.
Source: §4 · p. 11The approach does not accommodate the original PPSZ algorithm; improving it to do so is left as an open direction.
Source: §4 · p. 11
Abstract
from arXiv · showhide
The PPSZ algorithm by Paturi, Pudl\'ak, Saks, and Zane [1998] is the fastest known algorithm for Unique k-SAT, where the input formula does not have more than one satisfying assignment. For k>=5 the same bounds hold for general k-SAT. We show that this is also the case for k=3,4, using a slightly modified PPSZ algorithm. We do the analysis by defining a cost for satisfiable CNF formulas, which we prove to decrease in each PPSZ step by a certain amount. This improves our previous best bounds with Moser and Scheder [2011] for 3-SAT to O(1.308^n) and for 4-SAT to O(1.469^n).
1 Introduction
The introduction frames the gap between Unique 3-SAT and general 3-SAT running times, then presents a modified PPSZ analysis that extends the Unique-SAT bounds to k=3,4. Its key device is a cost for satisfiable formulas that decreases during PPSZ steps.
1 Introduction
- Paturi, Pudlák, Saks, and Zane gave a randomized Unique 3-SAT algorithm, running in O(1.30704^n) for formulas promised unique or unsatisfiable, versus the then-best general 3-SAT bound O(1.32065^n).Source: §1 · p. 1
1.1 Our Contribution
- O(1.30704^n) for 3-SAT and O(1.46899^n) for 4-SAT are the resulting randomized algorithm bounds.These improve the previous bounds of O(1.32065^n) and O(1.46928^n), respectively.Source: §1.1 · p. 2
- The analysis assigns each satisfiable formula a cost at most S·n and proves a lower bound of 2^-c(F) on PPSZ’s success probability.The cost decreases at each step; decreases are smaller when some variables are non-frozen, whose assignments preserve satisfiability with higher probability.Source: §1.1 · p. 2
1.2 Notation
- The notation section defines a CNF formula as a clause set paired with its variable set, and n(F) as the number of variables.It also defines assignments, satisfaction, and (≤k)-CNF formulas.Source: §1.2 · pp. 2–3
2 The PPSZ Algorithm
The paper modifies PPSZ by replacing bounded resolution with s-implication and immediately assigning all implied literals. Its analysis uses frozen-variable guessing bounds and properties of guessing probabilities under restrictions to establish the general k-SAT result.
2 The PPSZ Algorithm
- A literal is s-implied when some subformula with at most s clauses forces it in every satisfying assignment.The modified preprocessing uses this criterion instead of s-bounded resolution.Source: §2 · p. 3
- The algorithm immediately assigns all s-implied literals after each step, rather than processing variables strictly one by one.The authors say this modification strengthens the algorithm, while replacing bounded resolution with s-implication weakens it; the resulting algorithm runs in polynomial time for constant s.Source: §2 · p. 4
- For a frozen variable, the probability it is guessed is at most S_k + ε_k(s), extending the Unique-SAT guessing bound to arbitrary satisfying assignments.The proof uses s-implication in place of the earlier bounded-resolution preprocessing.Source: §2 · pp. 4–5
- The paper proves that general k-SAT has the same bound as Unique k-SAT for all k, using an algorithm that immediately fixes implied variables.For k≥5, the result is presented as an alternative proof of an already known bound.Source: §2 · p. 5
- Restricting a formula by a satisfying literal cannot increase the probability that a variable is guessed.The analysis also relates a variable’s guessing probability to its probability after a random satisfying-literal restriction.Source: §2 · pp. 5–6
3 Analysis using a Cost Function
The section defines a cost for satisfiable formulas using a distribution over their satisfying assignments, then uses cost reduction in PPSZ steps to bound its success probability. The proof handles s-implied literals separately and establishes the stepwise decrease through two lemmas.
3 Analysis using a Cost Function
- AssignSL repeatedly chooses a satisfying literal and restricts the formula, producing a distribution over satisfying assignments that need not be uniform.For x ∨ y, the all-true assignment has probability 1/4, while each assignment with exactly one variable set to 0 has probability 3/8.Source: §3 · pp. 6–7
- The cost is defined using p(F, α) and the probability that a frozen variable is guessed; non-frozen variables have cost S.The resulting variable costs are bounded by S.Source: §3 · p. 7, §3.1 · p. 9
- The cost function gives a lower bound on PPSZ’s success probability, and the analysis uses it to derive the claimed algorithmic bounds.Each variable’s cost is at most S, so c(F) ≤ n(F)S.Source: §3 · p. 7
- When a literal is s-implied, it is over a frozen variable, and fixing it does not increase the cost used in the inductive success-probability bound.The proof reduces to an s-implication-free formula when applying the one-step result.Source: §3 · pp. 7–8
- For an s-implication-free formula, the expected cost decrease depends on the frozen-variable mix: it is 1 when all variables are frozen and S when all are non-frozen.The non-frozen case has decrease S < 1.Source: §3 · pp. 7–8
3.1 Remaining Proofs
- The remaining proof uses separate lemmas for non-frozen variables and frozen variables that are not s-implied to establish the one-step bound.The lemma for non-frozen variables also holds when s-implied literals are present, though the proof uses it only for s-implication-free formulas.Source: §3.1 · p. 9
4 Conclusion
The adapted PPSZ analysis makes the general k-SAT bounds match the Unique k-SAT bounds, improving the 3-SAT and 4-SAT running times. The conclusion also identifies a boundary of the cost approach and a possible direction toward derandomization.
4 Conclusion
- O(1.30704n) improves the 3-SAT running-time bound from O(1.32065n); the general k-SAT bounds now match the Unique k-SAT bounds.For k ≥ 5, matching bounds were already known; the conclusion says the 3-SAT improvement is significant.Source: §4 · p. 11
- For k ≥ 5, the matching general and Unique k-SAT bounds were already known, though the authors describe their analysis as potentially more intuitive.Whether the bounds match in general remains open, as conjectured by Calabro et al..Source: §4 · p. 11
- The authors suggest that their generalization from Unique k-SAT might help derandomize PPSZ for general k-SAT.The passage contrasts this possibility with existing derandomization results for Schöning’s algorithm and Unique k-SAT.Source: §4 · p. 11
- The approach needs PPSZ to immediately use s-implied literals; the authors leave adapting the cost analysis to original PPSZ as an open possibility.In original PPSZ, s-implied variables have zero cost reduction, whereas the approach requires a positive minimum reduction.Source: §4 · p. 11