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}
}
Keywords: 

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

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

2017 
Date of publication: 

07.07.2017 