eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2020-07-17
3:1
3:12
10.4230/LIPIcs.CCC.2020.3
article
Super Strong ETH Is True for PPSZ with Small Resolution Width
Scheder, Dominik
1
Talebanfard, Navid
2
https://orcid.org/0000-0002-3524-9282
Shanghai Jiaotong University, China
Institute of Mathematics, The Czech Academy of Sciences, Prague, Czech Republic
We construct k-CNFs with m variables on which the strong version of PPSZ k-SAT algorithm, which uses resolution of width bounded by O(√{log log m}), has success probability at most 2^{-(1-(1 + ε)2/k)m} for every ε > 0. Previously such a bound was known only for the weak PPSZ algorithm which exhaustively searches through small subformulas of the CNF to see if any of them forces the value of a given variable, and for strong PPSZ the best known previous upper bound was 2^{-(1-O(log(k)/k))m} (Pudlák et al., ICALP 2017).
https://drops.dagstuhl.de/storage/00lipics/lipics-vol169-ccc2020/LIPIcs.CCC.2020.3/LIPIcs.CCC.2020.3.pdf
k-SAT
PPSZ
Resolution