PPSZ is better than you think

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 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 𝑘 ≥ 3.

We achieve this through an improved analysis and without any change to the algorithm itself.

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 while running the original algorithm, which does use a uniformly random order. like Schöning's algorithm [17] and random restriction algorithms like PPZ (Paturi, Pudl ák, and Zane [9]) and PPSZ (Paturi, Pudl ák, Saks, and Zane [8]). Both have a string of subsequent improvements: Hofmeister, Schöning, Schuler, and Watanabe [6], Baumer and Schuler [1], and An extended abstract of this work has already been published [12], and a full version is publicly accessible at [13].