Tighter Hard Instances for PPSZ

Abstract

We construct uniquely satisfiable $k$-CNF formulas that are hard for the PPSZ algorithm, the currently best known algorithm solving $k$-SAT. This algorithm tries to generate a satisfying assignment by picking a random variable at a time and attempting to derive its value using some inference heuristic and otherwise assigning a random value. The weak PPSZ checks all subformulas of a given size to derive a value and the strong PPSZ runs resolution with width bounded by some given function. Firstly, we construct graph-instances on which weak PPSZ has savings of at most $(2 + \epsilon)/k$; the saving of an algorithm on an input formula with $n$ variables is the largest gamma such that the algorithm succeeds (i.e. finds a satisfying assignment) with probability at least $2^{- (1 - \gamma) n}$. Since PPSZ (both weak and strong) is known to have savings of at least $(\pi^2 + o(1))/{6k}$, this is optimal up to the constant factor. In particular, for k=3, our upper bound is $2^{0.333… n}$, which is fairly close to the lower bound $2^{0.386… n}$ of Hertli [SIAM J. Comput.‘14]. We also construct instances based on linear systems over $F_{2}$ for which strong PPSZ has savings of at most $O(\log(k)/k)$. This is only a $\log(k)$ factor away from the optimal bound. Our constructions improve previous savings upper bound of $O((\log^2(k))/k)$ due to Chen et al. [SODA'13].

Publication
The 44th International Colloquium on Automata, Languages, and Programming (ICALP)
Date