PPSZ is better than you think
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.
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