Document Open Access Logo

Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs

Authors Susanna F. de Rezende , Jakob Nordström , Kilian Risse , Dmitry Sokolov

PDF

File

Thumbnail PDF
PDF
LIPIcs.CCC.2020.28.pdf
  • Filesize: 0.6 MB
  • 24 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • proof complexity
  • resolution
  • weak pigeonhole principle
  • perfect matching
  • sparse graphs

Metrics

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

Abstract

We show exponential lower bounds on resolution proof length for pigeonhole principle (PHP) formulas and perfect matching formulas over highly unbalanced, sparse expander graphs, thus answering the challenge to establish strong lower bounds in the regime between balanced constant-degree expanders as in [Ben-Sasson and Wigderson '01] and highly unbalanced, dense graphs as in [Raz '04] and [Razborov '03, '04]. We obtain our results by revisiting Razborov’s pseudo-width method for PHP formulas over dense graphs and extending it to sparse graphs. This further demonstrates the power of the pseudo-width method, and we believe it could potentially be useful for attacking also other longstanding open problems for resolution and other proof systems.

Cite As Get BibTex

Susanna F. de Rezende, Jakob Nordström, Kilian Risse, and Dmitry Sokolov. Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 28:1-28:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.CCC.2020.28

Author Details

Susanna F. de Rezende
  • Institute of Mathematics of the Czech Academy of Sciences, Prague, Czech Republic
Jakob Nordström
  • University of Copenhagen, Denmark
  • Lund University, Sweden
Kilian Risse
  • KTH Royal Institute of Technology, Stockholm, Sweden
Dmitry Sokolov
  • St. Petersburg State University, Russia
  • St. Petersburg Department of Steklov Mathematical Institute of Russian Academy of Sciences, Russia

Funding

The authors were funded by the Knut and Alice Wallenberg grant KAW 2016.0066. In addition, the second author was supported by the Swedish Research Council grant 2016-00782 and the Independent Research Fund Denmark (DFF) grant 9040-00389B, and the fourth author by the Knut and Alice Wallenberg grant KAW 2016.0433. Part of this work was carried out while visiting the Simons Institute for the Theory of Computing in association with the DIMACS/Simons Collaboration on Lower Bounds in Computational Complexity, which is conducted with support from the National Science Foundation.

Acknowledgements

First and foremost, we are most grateful to Alexander Razborov for many discussions about pseudo-width, graph closure, and other mysteries of the universe. We also thank Paul Beame and Johan Håstad for useful discussions, and Jonah Brown-Cohen for helpful references on expander graphs. Finally, we gratefully acknowledge the feedback from participants of the Dagstuhl workshop 19121 Computational Complexity of Discrete Problems in March 2019.

References

  1. Michael Alekhnovich. Mutilated chessboard problem is exponentially hard for resolution. Theoretical Computer Science, 310(1-3):513-525, January 2004. Google Scholar
  2. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Space complexity in propositional calculus. SIAM Journal on Computing, 31(4):1184-1211, 2002. Preliminary version in STOC '00. Google Scholar
  3. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Pseudorandom generators in propositional proof complexity. SIAM Journal on Computing, 34(1):67-88, 2004. Preliminary version in FOCS '00. Google Scholar
  4. Michael Alekhnovich and Alexander A. Razborov. Lower bounds for polynomial calculus: Non-binomial case. Proceedings of the Steklov Institute of Mathematics, 242:18-35, 2003. Available at http://people.cs.uchicago.edu/~razborov/files/misha.pdf. Preliminary version in FOCS '01.
  5. Albert Atserias, Ilario Bonacina, Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Alexander Razborov. Clique is hard on average for regular resolution. In Proceedings of the 50th Annual ACM Symposium on Theory of Computing (STOC '18), pages 866-877, June 2018. Google Scholar
  6. Paul Beame, Russell Impagliazzo, and Ashish Sabharwal. The resolution complexity of independent sets and vertex covers in random graphs. Computational Complexity, 16(3):245-297, October 2007. Preliminary version in CCC '01. Google Scholar
  7. Paul Beame and Toniann Pitassi. Simplified and improved resolution lower bounds. In Proceedings of the 37th Annual IEEE Symposium on Foundations of Computer Science (FOCS '96), pages 274-282, October 1996. Google Scholar
  8. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. Journal of the ACM, 48(2):149-169, March 2001. Preliminary version in STOC '99. 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. Information Processing Letters, 110(23):1074-1077, 2010. URL: https://doi.org/10.1016/j.ipl.2010.09.007.
  10. Archie Blake. Canonical Expressions in Boolean Algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  11. Samuel R. Buss and Toniann Pitassi. Resolution and the weak pigeonhole principle. In 11th International Workshop on Computer Science Logic (CSL '97), Selected Papers, volume 1414 of Lecture Notes in Computer Science, pages 149-156. Springer, August 1997. Google Scholar
  12. Samuel R. Buss and Győrgy Turán. Resolution proofs of generalized pigeonhole principles. Theoretical Computer Science, 62(3):311-317, December 1988. Google Scholar
  13. Vašek Chvátal and Endre Szemerédi. Many hard examples for resolution. Journal of the ACM, 35(4):759-768, October 1988. Google Scholar
  14. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the 28th Annual ACM Symposium on Theory of Computing (STOC '96), pages 174-183, May 1996. Google Scholar
  15. Stefan S. Dantchev. Resolution width-size trade-offs for the pigeon-hole principle. In Proceedings of the 17th Annual IEEE Conference on Computational Complexity (CCC '02), pages 39-43, May 2002. URL: https://doi.org/10.1109/CCC.2002.1004337.
  16. Stefan S. Dantchev and Søren Riis. "Planar" tautologies hard for resolution. In Proceedings of the 42nd Annual IEEE Symposium on Foundations of Computer Science (FOCS '01), pages 220-229, October 2001. Google Scholar
  17. 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 (CCC '01), pages 69-75, June 2001. URL: https://doi.org/10.1109/CCC.2001.933873.
  18. Venkatesan Guruswami, Christopher Umans, and Salil Vadhan. Unbalanced expanders and randomness extractors from Parvaresh-Vardy codes. Journal of the ACM, 56(4):20:1-20:34, July 2009. Preliminary version in CCC '07. Google Scholar
  19. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39(2-3):297-308, August 1985. Google Scholar
  20. Dmitry Itsykson, Vsevolod Oparin, Mikhail Slabodkin, and Dmitry Sokolov. Tight lower bounds on the resolution complexity of perfect matching principles. Fundamenta Informaticae, 145(3):229-242, August 2016. URL: https://doi.org/10.3233/FI-2016-1358.
  21. Shuo Pang. Large clique is hard on average for resolution. Technical Report TR19-068, Electronic Colloquium on Computational Complexity (ECCC), April 2019. Google Scholar
  22. Toniann Pitassi and Ran Raz. Regular resolution lower bounds for the weak pigeonhole principle. Combinatorica, 24(3):503-524, 2004. Preliminary version in STOC '01. URL: https://doi.org/10.1007/s00493-004-0030-y.
  23. Ran Raz. Resolution lower bounds for the weak pigeonhole principle. Journal of the ACM, 51(2):115-138, March 2004. Preliminary version in STOC '02. Google Scholar
  24. Alexander A. Razborov. Lower bounds for the polynomial calculus. Computational Complexity, 7(4):291-324, December 1998. Google Scholar
  25. Alexander A. Razborov. Improved resolution lower bounds for the weak pigeonhole principle. Technical Report TR01-055, Electronic Colloquium on Computational Complexity (ECCC), July 2001. Google Scholar
  26. Alexander A. Razborov. Proof complexity of pigeonhole principles. In 5th International Conference on Developments in Language Theory, (DLT '01), Revised Papers, volume 2295 of Lecture Notes in Computer Science, pages 100-116. Springer, July 2002. Google Scholar
  27. Alexander A. Razborov. Resolution lower bounds for the weak functional pigeonhole principle. Theoretical Computer Science, 1(303):233-243, June 2003. Google Scholar
  28. Alexander A. Razborov. Resolution lower bounds for perfect matching principles. Journal of Computer and System Sciences, 69(1):3-27, August 2004. Preliminary version in CCC '02. Google Scholar
  29. Alexander A. Razborov. Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Annals of Mathematics, 181(2):415-472, March 2015. Google Scholar
  30. Alexander A. Razborov, Avi Wigderson, and Andrew Chi-Chih Yao. Read-once branching programs, rectangular proofs of the pigeonhole principle and the transversal calculus. Combinatorica, 22(4):555-574, 2002. Preliminary version in STOC '97. URL: https://doi.org/10.1007/s00493-002-0007-7.
  31. Alasdair Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209-219, January 1987. Google Scholar
  32. Alasdair Urquhart. Resolution proofs of matching principles. Annals of Mathematics and Artificial Intelligence, 37(3):241-250, March 2003. URL: https://doi.org/10.1023/A:1021231610627.
  33. Alasdair Urquhart. Width versus size in resolution proofs. Theoretical Computer Science, 384(1):104-110, September 2007. Google Scholar
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact