Pudlák, Pavel ;
Scheder, Dominik ;
Talebanfard, Navid
Tighter Hard Instances for PPSZ
Abstract
We construct uniquely satisfiable kCNF formulas that are hard for the PPSZ algorithm, the currently best known algorithm solving kSAT. 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 graphinstances 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].
BibTeX  Entry
@InProceedings{pudlk_et_al:LIPIcs:2017:7414,
author = {Pavel Pudl{\'a}k and Dominik Scheder and Navid Talebanfard},
title = {{Tighter Hard Instances for PPSZ}},
booktitle = {44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
pages = {85:185:13},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770415},
ISSN = {18688969},
year = {2017},
volume = {80},
editor = {Ioannis Chatzigiannakis and Piotr Indyk and Fabian Kuhn and Anca Muscholl},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7414},
URN = {urn:nbn:de:0030drops74144},
doi = {10.4230/LIPIcs.ICALP.2017.85},
annote = {Keywords: kSAT, Strong Exponential Time Hypothesis, PPSZ, Resolution}
}
07.07.2017
Keywords: 

kSAT, Strong Exponential Time Hypothesis, PPSZ, Resolution 
Seminar: 

44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Issue date: 

2017 
Date of publication: 

07.07.2017 