Tighter Hard Instances for PPSZ

Authors Pavel Pudlák, Dominik Scheder, Navid Talebanfard

Thumbnail PDF


  • Filesize: 0.56 MB
  • 13 pages

Document Identifiers

Author Details

Pavel Pudlák
Dominik Scheder
Navid Talebanfard

Cite AsGet BibTex

Pavel Pudlák, Dominik Scheder, and Navid Talebanfard. Tighter Hard Instances for PPSZ. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 85:1-85:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


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].
  • k-SAT
  • Strong Exponential Time Hypothesis
  • PPSZ
  • Resolution


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Arturs Backurs and Piotr Indyk. Edit distance cannot be computed in strongly subquadratic time (unless SETH is false). In Rocco A. Servedio and Ronitt Rubinfeld, editors, Proceedings of the Forty-Seventh Annual ACM on Symposium on Theory of Computing, STOC 2015, Portland, OR, USA, June 14-17, 2015, pages 51-58. ACM, 2015. URL: http://dl.acm.org/citation.cfm?id=2746539, URL: http://dx.doi.org/10.1145/2746539.2746612.
  2. Eli Ben-Sasson and Russell Impagliazzo. Random cnf’s are hard for the polynomial calculus. Computational Complexity, 19(4):501-519, 2010. URL: http://dx.doi.org/10.1007/s00037-010-0293-1.
  3. Shiteng Chen, Dominik Scheder, Navid Talebanfard, and Bangsheng Tang. Exponential lower bounds for the PPSZ k-SAT algorithm. In Sanjeev Khanna, editor, Proceedings of the Twenty-Fourth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2013, New Orleans, Louisiana, USA, January 6-8, 2013, pages 1253-1263. SIAM, 2013. URL: http://dx.doi.org/10.1137/1.9781611973105.91.
  4. Evgeny Dantsin, Andreas Goerdt, Edward A. Hirsch, Ravi Kannan, Jon M. Kleinberg, Christos H. Papadimitriou, Prabhakar Raghavan, and Uwe Schöning. A deterministic (2-2/(k+1))^n algorithm for k-sat based on local search. Theor. Comput. Sci., 289(1):69-83, 2002. URL: http://dx.doi.org/10.1016/S0304-3975(01)00174-8.
  5. Paul Erdős and Horst Sachs. Reguläre Graphen gegebener Taillenweite mit minimaler Knotenzahl. (Regular graphs with given girth and minimal number of knots.). Wiss. Z. Martin-Luther-Univ. Halle-Wittenberg, Math.-Naturwiss., 12:251-258, 1963. Google Scholar
  6. Timon Hertli. 3-sat faster and simpler - unique-sat bounds for PPSZ hold in general. SIAM J. Comput., 43(2):718-729, 2014. URL: http://dx.doi.org/10.1137/120868177.
  7. Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-sat. J. Comput. Syst. Sci., 62(2):367-375, 2001. URL: http://dx.doi.org/10.1006/jcss.2000.1727.
  8. Daniel Lokshtanov, Dániel Marx, and Saket Saurabh. Lower bounds based on the exponential time hypothesis. Bulletin of the EATCS, 105:41-72, 2011. URL: http://albcom.lsi.upc.edu/ojs/index.php/beatcs/article/view/96.
  9. Alexander Lubotzky, Ralph Phillips, and Peter Sarnak. Ramanujan graphs. Combinatorica, 8(3):261-277, 1988. URL: http://dx.doi.org/10.1007/BF02126799.
  10. Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, and Francis Zane. An improved exponential-time algorithm for k-sat. J. ACM, 52(3):337-364, 2005. URL: http://dx.doi.org/10.1145/1066100.1066101.
  11. Ramamohan Paturi, Pavel Pudlák, and Francis Zane. Satisfiability coding lemma. Chicago J. Theor. Comput. Sci., 1999, 1999. URL: http://cjtcs.cs.uchicago.edu/articles/1999/11/contents.html.
  12. Uwe Schöning. A probabilistic algorithm for k-sat and constraint satisfaction problems. In 40th Annual Symposium on Foundations of Computer Science, FOCS'99, 17-18 October, 1999, New York, NY, USA, pages 410-414. IEEE Computer Society, 1999. URL: http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=6604, URL: http://dx.doi.org/10.1109/SFFCS.1999.814612.
  13. G. S. Tseitin. On the complexity of derivation in propositional calculus. Studies in Constructive Mathematics and Mathematical Logic, (2):115-125, 1968. Google Scholar
  14. Alasdair Urquhart. Hard examples for resolution. J. ACM, 34(1):209-219, 1987. URL: http://dx.doi.org/10.1145/7531.8928.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail