Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

PPSZ is better than you think

Dominik Scheder

TL;DR

This work analyzes the PPSZ algorithm for $k$-SAT not by altering the algorithm itself, but by introducing a carefully designed make-believe distribution over variable orders and leveraging KL-divergence penalties to bound the gain. By studying canonical critical clause trees and introducing labeled-tree machinery, the authors prove an exponential improvement in PPSZ’s success probability for all $k\ge3$, and derive a lifting result that extends Unique-$k$-SAT gains to general $k$-SAT. In particular, Unique-$3$-SAT is shown to run in time $O(1.306973^n)$, tightening prior bounds, while the framework clarifies how structure in the CNF formula yields additional forcing leverage without modifying the algorithm. The techniques combine Jensen-type bounds with structured distributions that emphasize variables appearing in many critical clauses, yielding positive gains via heavy-variable bonuses and disjoint-pair constructions, and offering a modular path to further improvements in PPSZ analyses.

Abstract

PPSZ, for long time the fastest known algorithm for $k$-SAT, works by going through the variables of the input formula in random order; each variable is then set randomly to $0$ or $1$, unless the correct value can be inferred by an efficiently implementable rule (like small-width resolution; or being implied by a small set of clauses). We show that PPSZ performs exponentially better than previously known, for all $k \geq 3$. For Unique-$3$-SAT we bound its running time by $O(1.306973^{n})$, which is somewhat better than the algorithm of Hansen, Kaplan, Zamir, and Zwick, which runs in time $O(1.306995^n)$. Before that, the best known upper bound for Unique-$3$-SAT was $O(1.3070319^n)$. All improvements are achieved without changing the original PPSZ. The core idea is to pretend that PPSZ does not process the variables in uniformly random order, but according to a carefully designed distribution. We write "pretend" since this can be done without any actual change to the algorithm.

PPSZ is better than you think

TL;DR

This work analyzes the PPSZ algorithm for -SAT not by altering the algorithm itself, but by introducing a carefully designed make-believe distribution over variable orders and leveraging KL-divergence penalties to bound the gain. By studying canonical critical clause trees and introducing labeled-tree machinery, the authors prove an exponential improvement in PPSZ’s success probability for all , and derive a lifting result that extends Unique--SAT gains to general -SAT. In particular, Unique--SAT is shown to run in time , tightening prior bounds, while the framework clarifies how structure in the CNF formula yields additional forcing leverage without modifying the algorithm. The techniques combine Jensen-type bounds with structured distributions that emphasize variables appearing in many critical clauses, yielding positive gains via heavy-variable bonuses and disjoint-pair constructions, and offering a modular path to further improvements in PPSZ analyses.

Abstract

PPSZ, for long time the fastest known algorithm for -SAT, works by going through the variables of the input formula in random order; each variable is then set randomly to or , unless the correct value can be inferred by an efficiently implementable rule (like small-width resolution; or being implied by a small set of clauses). We show that PPSZ performs exponentially better than previously known, for all . For Unique--SAT we bound its running time by , which is somewhat better than the algorithm of Hansen, Kaplan, Zamir, and Zwick, which runs in time . Before that, the best known upper bound for Unique--SAT was . All improvements are achieved without changing the original PPSZ. The core idea is to pretend that PPSZ does not process the variables in uniformly random order, but according to a carefully designed distribution. We write "pretend" since this can be done without any actual change to the algorithm.
Paper Structure (25 sections, 13 theorems, 27 equations, 1 figure, 2 algorithms)

This paper contains 25 sections, 13 theorems, 27 equations, 1 figure, 2 algorithms.

Table of Contents

  1. Introduction
  2. Analyzing PPSZ: permutations and forced variables
  3. The PPSZ algorithm with strength parameter $w$.
  4. Previous improvements
  5. Multiple satisfying assignments.
  6. Improved algorithms.
  7. Lower bounds.
  8. Our contribution
  9. Comparison to Hansen et al.
  10. The case k=3
  11. Organization of the paper
  12. Brief overview of our method
  13. Working with a make-belief distribution on permutations
  14. Good make-belief distributions for PPSZ---a rough sketch
  15. Critical clause trees, labeled trees, and cuts
  16. ...and 10 more sections

Key Result

Theorem 1.3

If $F$ is a $k$-CNF formula with a unique satisfying assignment, then Furthermore, $s_k = \frac{\pi^2}{6k} + o(1/k)$.

Figures (1)

  • Figure 4: A labeled tree, a placement, and a cut, a non-cut and a weak cut.

Theorems & Definitions (22)

  • definition 1.1
  • Theorem 1.3: ppsz
  • Theorem 1.4: Unique-to-General lifting theorem ppsz
  • Theorem 1.5: Improvement for all $k$
  • Lemma 3.2: ppsz
  • definition 3.3: Canonical critical clause
  • definition 3.4: Canonical critical clause tree, CCCT
  • definition 3.5: Canonical nodes
  • definition 3.6: Labeled trees
  • definition 3.7: ${\rm Cut}$ and ${\rm Cut}_r$ and $\textnormal{wCut}_r$
  • ...and 12 more