Tighter Hard Instances for PPSZ

0476174 - MÚ 2018 RIV DE eng C - Konferenční příspěvek (zahraniční konf.)
Pudlák, Pavel - Scheder, D. - Talebanfard, Navid
Tighter Hard Instances for PPSZ.
44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Dagstuhl: Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2017 - (Chatzigiannakis, I.; Indyk, P.; Kuhn, F.; Muscholl, A.), s. 1-13, č. článku 85. Leibniz International Proceedings in Informatics, 80. ISBN 978-3-95977-041-5. ISSN 1868-8969.
[44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Warsaw (PL), 10.07.2017-14.07.2017]
Grant CEP: GA ČR GBP202/12/G061
Institucionální podpora: RVO:67985840
Klíčová slova: k-SAT * strong exponential time hypothesis * PPSZ * resolution
Obor OECD: Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=7414

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.
Trvalý link: http://hdl.handle.net/11104/0272702