English

PPSZ is better than you think

Data Structures and Algorithms 2024-08-07 v2

Abstract

PPSZ, for long time the fastest known algorithm for kk-SAT, works by going through the variables of the input formula in random order; each variable is then set randomly to 00 or 11, 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 k3k \geq 3. For Unique-33-SAT we bound its running time by O(1.306973n)O(1.306973^{n}), which is somewhat better than the algorithm of Hansen, Kaplan, Zamir, and Zwick, which runs in time O(1.306995n)O(1.306995^n). Before that, the best known upper bound for Unique-33-SAT was O(1.3070319n)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.

Keywords

Cite

@article{arxiv.2207.11071,
  title  = {PPSZ is better than you think},
  author = {Dominik Scheder},
  journal= {arXiv preprint arXiv:2207.11071},
  year   = {2024}
}

Comments

Journal version of this work. The previous arxiv version is the "full version", which contains the proof for the k=3 case

R2 v1 2026-06-25T01:08:47.659Z