Document Open Access Logo

Resolution and the Binary Encoding of Combinatorial Principles

Authors Stefan Dantchev, Nicola Galesi, Barnaby Martin

PDF
Thumbnail PDF

File

LIPIcs.CCC.2019.6.pdf
  • Filesize: 0.67 MB
  • 25 pages

Document Identifiers

Author Details

Stefan Dantchev
  • Department of Computer Science University of Durham, UK
Nicola Galesi
  • Dipartimento di Informatica, Sapienza Università di Roma, Italy
Barnaby Martin
  • Department of Computer Science University of Durham, UK

Acknowledgements

We are grateful to Ilario Bonacina for reading a preliminary version of this work and addressing us some useful comments and observations. We are further grateful to several anonymous reviewers for further corrections and comments.

Cite AsGet BibTex

Stefan Dantchev, Nicola Galesi, and Barnaby Martin. Resolution and the Binary Encoding of Combinatorial Principles. In 34th Computational Complexity Conference (CCC 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 137, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CCC.2019.6

Abstract

Res(s) is an extension of Resolution working on s-DNFs. We prove tight n^{Omega(k)} lower bounds for the size of refutations of the binary version of the k-Clique Principle in Res(o(log log n)). Our result improves that of Lauria, Pudlák et al. [Massimo Lauria et al., 2017] who proved the lower bound for Res(1), i.e. Resolution. The exact complexity of the (unary) k-Clique Principle in Resolution is unknown. To prove the lower bound we do not use any form of the Switching Lemma [Nathan Segerlind et al., 2004], instead we apply a recursive argument specific for binary encodings. Since for the k-Clique and other principles lower bounds in Resolution for the unary version follow from lower bounds in Res(log n) for their binary version we start a systematic study of the complexity of proofs in Resolution-based systems for families of contradictions given in the binary encoding. We go on to consider the binary version of the weak Pigeonhole Principle Bin-PHP^m_n for m>n. Using the the same recursive approach we prove the new result that for any delta>0, Bin-PHP^m_n requires proofs of size 2^{n^{1-delta}} in Res(s) for s=o(log^{1/2}n). Our lower bound is almost optimal since for m >= 2^{sqrt{n log n}} there are quasipolynomial size proofs of Bin-PHP^m_n in Res(log n). Finally we propose a general theory in which to compare the complexity of refuting the binary and unary versions of large classes of combinatorial principles, namely those expressible as first order formulae in Pi_2-form and with no finite model.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity theory and logic
Keywords
  • Proof complexity
  • k-DNF resolution
  • binary encodings
  • Clique and Pigeonhole principle

Metrics

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

References

  1. Michael Alekhnovich. Lower Bounds for k-DNF Resolution on Random 3-CNFs. Computational Complexity, 20(4):597-614, 2011. URL: https://doi.org/10.1007/s00037-011-0026-0.
  2. Razborov Alexander A. Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Annals of Mathematics, 181(41):415-472, 2015. Google Scholar
  3. Albert Atserias. Improved bounds on the Weak Pigeonhole Principle and infinitely many primes from weaker axioms. Theor. Comput. Sci., 295:27-39, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00394-8.
  4. Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Alexander A. Razborov. Clique is hard on average for regular resolution. In Ilias Diakonikolas, David Kempe, and Monika Henzinger, editors, Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, Los Angeles, CA, USA, June 25-29, 2018, pages 866-877. ACM, 2018. URL: https://doi.org/10.1145/3188745.3188856.
  5. Albert Atserias, Maria Luisa Bonet, and Juan Luis Esteban. Lower Bounds for the Weak Pigeonhole Principle and Random Formulas beyond Resolution. Inf. Comput., 176(2):136-152, 2002. URL: https://doi.org/10.1006/inco.2002.3114.
  6. Paul Beame, Russell Impagliazzo, and Ashish Sabharwal. Resolution Complexity of Independent Sets in Random Graphs. In Proceedings of the 16th Annual IEEE Conference on Computational Complexity, Chicago, Illinois, USA, June 18-21, 2001, pages 52-68. IEEE Computer Society, 2001. URL: https://doi.org/10.1109/CCC.2001.933872.
  7. Paul Beame and Toniann Pitassi. Simplified and Improved Resolution Lower Bounds. In 37th Annual Symposium on Foundations of Computer Science, FOCS '96, Burlington, Vermont, USA, 14-16 October, 1996, pages 274-282. IEEE Computer Society, 1996. URL: https://doi.org/10.1109/SFCS.1996.548486.
  8. Eli Ben-sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. In Journal of the ACM, pages 517-526, 1999. Google Scholar
  9. Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. A lower bound for the pigeonhole principle in tree-like Resolution by asymmetric Prover-Delayer games. Inf. Process. Lett., 110(23):1074-1077, 2010. URL: https://doi.org/10.1016/j.ipl.2010.09.007.
  10. Olaf Beyersdorff, Nicola Galesi, and Massimo Lauria. Parameterized Complexity of DPLL Search Procedures. ACM Trans. Comput. Logic, 14(3):20:1-20:21, August 2013. URL: https://doi.org/10.1145/2499937.2499941.
  11. Olaf Beyersdorff, Nicola Galesi, Massimo Lauria, and Alexander A. Razborov. Parameterized Bounded-Depth Frege Is not Optimal. TOCT, 4(3):7:1-7:16, 2012. URL: https://doi.org/10.1145/2355580.2355582.
  12. Ilario Bonacina and Nicola Galesi. A Framework for Space Complexity in Algebraic Proof Systems. J. ACM, 62(3):23:1-23:20, 2015. URL: https://doi.org/10.1145/2699438.
  13. Ilario Bonacina, Nicola Galesi, and Neil Thapen. Total Space in Resolution. SIAM J. Comput., 45(5):1894-1909, 2016. URL: https://doi.org/10.1137/15M1023269.
  14. Maria Luisa Bonet and Nicola Galesi. Optimality of size-width tradeoffs for resolution. Computational Complexity, 10(4):261-276, 2001. URL: https://doi.org/10.1007/s000370100000.
  15. Samuel R. Buss and Toniann Pitassi. Resolution and the Weak Pigeonhole Principle. In Computer Science Logic, 11th International Workshop, CSL '97, Annual Conference of the EACSL, Aarhus, Denmark, August 23-29, 1997, Selected Papers, pages 149-156, 1997. URL: https://doi.org/10.1007/BFb0028012.
  16. Stefan S. Dantchev and Søren Riis. Tree Resolution Proofs of the Weak Pigeon-Hole Principle. In Proceedings of the 16th Annual IEEE Conference on Computational Complexity, Chicago, Illinois, USA, June 18-21, 2001, pages 69-75, 2001. URL: https://doi.org/10.1109/CCC.2001.933873.
  17. Stefan S. Dantchev and Søren Riis. On Relativisation and Complexity Gap. In Matthias Baaz and Johann A. Makowsky, editors, Computer Science Logic, 17th International Workshop, CSL 2003, 12th Annual Conference of the EACSL, and 8th Kurt Gödel Colloquium, KGC 2003, Vienna, Austria, August 25-30, 2003, Proceedings, volume 2803 of Lecture Notes in Computer Science, pages 142-154. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45220-1_14.
  18. Juan Luis Esteban, Nicola Galesi, and Jochen Messner. On the complexity of resolution with bounded conjunctions. Theor. Comput. Sci., 321(2-3):347-370, 2004. URL: https://doi.org/10.1016/j.tcs.2004.04.004.
  19. Yuval Filmus, Massimo Lauria, Jakob Nordström, Noga Ron-Zewi, and Neil Thapen. Space Complexity in Polynomial Calculus. SIAM J. Comput., 44(4):1119-1153, 2015. URL: https://doi.org/10.1137/120895950.
  20. Nicola Galesi and Massimo Lauria. Optimality of size-degree tradeoffs for polynomial calculus. ACM Trans. Comput. Log., 12(1):4:1-4:22, 2010. URL: https://doi.org/10.1145/1838552.1838556.
  21. Armin Haken. The Intractability of Resolution. Theor. Comput. Sci., 39:297-308, 1985. Google Scholar
  22. Pavel Hrubes and Pavel Pudlák. Random Formulas, Monotone Circuits, and Interpolation. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 121-131. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/FOCS.2017.20.
  23. Jan Krajíček. Bounded arithmetic, propositional logic and complexity theory. Cambridge University Press, 1995. Google Scholar
  24. Balakrishnan Krishnamurthy. Short Proofs for Tricky Formulas. Acta Inf., 22(3):253-275, 1985. URL: https://doi.org/10.1007/BF00265682.
  25. Oliver Kullmann. Investigating a general hierarchy of polynomially decidable classes of CNF’s based on short tree-like resolution proofs. Electronic Colloquium on Computational Complexity (ECCC), 41, 1999. URL: http://eccc.hpi-web.de/eccc-reports/1999/TR99-041/index.html.
  26. G. Kwon and W. Klieber. Efficient CNF Encoding for Selecting 1 from N Objects. In Fourth Workshop on Constraints in Formal Verification (CFV '07), 2007. Google Scholar
  27. Massimo Lauria, Pavel Pudlák, Vojtech Rödl, and Neil Thapen. The complexity of proving that a graph is Ramsey. Combinatorica, 37(2):253-268, 2017. URL: https://doi.org/10.1007/s00493-015-3193-9.
  28. Alexis Maciel, Toniann Pitassi, and Alan R. Woods. A New Proof of the Weak Pigeonhole Principle. J. Comput. Syst. Sci., 64(4):843-872, 2002. URL: https://doi.org/10.1006/jcss.2002.1830.
  29. Justyna Petke. Bridging Constraint Satisfaction and Boolean Satisfiability. Artificial Intelligence: Foundations, Theory, and Algorithms. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21810-6.
  30. P. Pudlák. Proofs as games. American Mathematical Monthly, pages 541-550, June-July 2000. Google Scholar
  31. Ran Raz. Resolution lower bounds for the weak pigeonhole principle. J. ACM, 51(2):115-138, 2004. URL: https://doi.org/10.1145/972639.972640.
  32. Alexander A. Razborov. Proof Complexity of Pigeonhole Principles. In Werner Kuich, Grzegorz Rozenberg, and Arto Salomaa, editors, Developments in Language Theory, pages 100-116, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. Google Scholar
  33. Alexander A. Razborov. Resolution lower bounds for the weak functional pigeonhole principle. Theor. Comput. Sci., 1(303):233-243, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00453-X.
  34. Søren Riis. A complexity gap for tree resolution. Computational Complexity, 10(3):179-209, 2001. URL: http://link.springer.de/link/service/journals/00037/bibs/1010003/10100179.htm.
  35. Nathan Segerlind, Samuel R. Buss, and Russell Impagliazzo. A Switching Lemma for Small Restrictions and Lower Bounds for k-DNF Resolution. SIAM J. Comput., 33(5):1171-1200, 2004. URL: https://doi.org/10.1137/S0097539703428555.
  36. Gunnar Stålmarck. Short Resolution Proofs for a Sequence of Tricky Formulas. Acta Inf., 33(3):277-280, 1996. URL: https://doi.org/10.1007/s002360050044.
  37. Toby Walsh. SAT v CSP. In Principles and Practice of Constraint Programming - CP 2000, 6th International Conference, Singapore, September 18-21, 2000, Proceedings, pages 441-456, 2000. URL: https://doi.org/10.1007/3-540-45349-0_32.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact