Document Open Access Logo

A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds

Authors Mladen Miksa, Jakob Nordström

PDF
Thumbnail PDF

File

LIPIcs.CCC.2015.467.pdf
  • Filesize: 0.53 MB
  • 21 pages

Document Identifiers

Author Details

Mladen Miksa
Jakob Nordström

Cite AsGet BibTex

Mladen Miksa and Jakob Nordström. A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds. In 30th Conference on Computational Complexity (CCC 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 33, pp. 467-487, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CCC.2015.467

Abstract

We study the problem of establishing lower bounds for polynomial calculus (PC) and polynomial calculus resolution (PCR) on proof degree, and hence by [Impagliazzo et al. '99] also on proof size. [Alekhnovich and Razborov '03] established that if the clause-variable incidence graph of a CNF formula F is a good enough expander, then proving that F is unsatisfiable requires high PC/PCR degree. We further develop the techniques in [AR03] to show that if one can "cluster" clauses and variables in a way that "respects the structure" of the formula in a certain sense, then it is sufficient that the incidence graph of this clustered version is an expander. As a corollary of this, we prove that the functional pigeonhole principle (FPHP) formulas require high PC/PCR degree when restricted to constant-degree expander graphs. This answers an open question in [Razborov '02], and also implies that the standard CNF encoding of the FPHP formulas require exponential proof size in polynomial calculus resolution.
Keywords
  • proof complexity
  • polynomial calculus
  • polynomial calculus resolution
  • PCR
  • degree
  • size
  • functional pigeonhole principle
  • lower bound

Metrics

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

References

  1. 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 appeared in STOC'00. Google Scholar
  2. 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 appeared in FOCS'01.
  3. Paul Beame, Joseph C. Culberson, David G. Mitchell, and Cristopher Moore. The resolution complexity of random graph k-colorability. Discrete Applied Mathematics, 153(1-3):25-47, December 2005. Google Scholar
  4. 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. Google Scholar
  5. 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 appeared in STOC'99. Google Scholar
  6. Archie Blake. Canonical Expressions in Boolean Algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  7. Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. Linear gaps between degrees for the polynomial calculus modulo distinct primes. Journal of Computer and System Sciences, 62(2):267-289, March 2001. Preliminary version appeared in CCC'99. Google Scholar
  8. 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
  9. 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
  10. Stephen A. Cook and Robert Reckhow. The relative efficiency of propositional proof systems. Journal of Symbolic Logic, 44(1):36-50, March 1979. Google Scholar
  11. Yuval Filmus. On the Alekhnovich-Razborov degree lower bound for the polynomial calculus. Manuscript. Available at http://www.cs.toronto.edu/~yuvalf/AlRa.pdf, 2014.
  12. Nicola Galesi and Massimo Lauria. Optimality of size-degree trade-offs for polynomial calculus. ACM Transactions on Computational Logic, 12:4:1-4:22, November 2010. Google Scholar
  13. Dima Grigoriev. Tseitin’s tautologies and lower bounds for Nullstellensatz proofs. In Proceedings of the 39th Annual IEEE Symposium on Foundations of Computer Science (FOCS'98), pages 648-652, November 1998. Google Scholar
  14. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39(2-3):297-308, August 1985. Google Scholar
  15. Shlomo Hoory, Nathan Linial, and Avi Wigderson. Expander graphs and their applications. Bulletin of the American Mathematical Society, 43(4):439-561, October 2006. Google Scholar
  16. Russell Impagliazzo, Pavel Pudlák, and Jiří Sgall. Lower bounds for the polynomial calculus and the Gröbner basis algorithm. Computational Complexity, 8(2):127-144, 1999. Google Scholar
  17. Mladen Mikša and Jakob Nordström. Long proofs of (seemingly) simple formulas. In Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT'14), volume 8561 of Lecture Notes in Computer Science, pages 121-137. Springer, July 2014. Google Scholar
  18. Mladen Mikša and Jakob Nordström. A generalized method for proving polynomial calculus degree lower bounds. Technical Report TR15-078, Electronic Colloquium on Computational Complexity (ECCC), May 2015. Google Scholar
  19. Jakob Nordström. Pebble games, proof complexity and time-space trade-offs. Logical Methods in Computer Science, 9:15:1-15:63, September 2013. Google Scholar
  20. Ran Raz. Resolution lower bounds for the weak pigeonhole principle. Journal of the ACM, 51(2):115-138, March 2004. Preliminary version appeared in STOC'02. Google Scholar
  21. Alexander A. Razborov. Lower bounds for the polynomial calculus. Computational Complexity, 7(4):291-324, December 1998. Google Scholar
  22. 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
  23. 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
  24. Alexander A. Razborov. Resolution lower bounds for the weak functional pigeonhole principle. Theoretical Computer Science, 1(303):233-243, June 2003. Google Scholar
  25. Alexander A. Razborov. Resolution lower bounds for perfect matching principles. Journal of Computer and System Sciences, 69(1):3-27, August 2004. Preliminary version appeared in CCC'02. Google Scholar
  26. Alexander A. Razborov. Possible research directions. List of open problems (in proof complexity and other areas) available at http://people.cs.uchicago.edu/~razborov/teaching/, 2014.
  27. Søren Riis. Independence in Bounded Arithmetic. PhD thesis, University of Oxford, 1993. Google Scholar
  28. Ivor Spence. sgen1: A generator of small but difficult satisfiability benchmarks. Journal of Experimental Algorithmics, 15:1.2:1.1-1.2:1.15, March 2010. Google Scholar
  29. Alasdair Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209-219, January 1987. Google Scholar
  30. Allen Van Gelder and Ivor Spence. Zero-one designs produce small hard SAT instances. In Proceedings of the 13th International Conference on Theory and Applications of Satisfiability Testing (SAT'10), volume 6175 of Lecture Notes in Computer Science, pages 388-397. Springer, July 2010. 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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact