Document Open Access Logo

Trade-Offs Between Size and Degree in Polynomial Calculus

Authors Guillaume Lagarde, Jakob Nordström , Dmitry Sokolov, Joseph Swernofsky

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITCS.2020.72.pdf
  • Filesize: 0.53 MB
  • 16 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • proof complexity
  • polynomial calculus
  • polynomial calculus resolution
  • PCR
  • size-degree trade-off
  • resolution
  • colored polynomial local search

Metrics

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

Abstract

Building on [Clegg et al. '96], [Impagliazzo et al. '99] established that if an unsatisfiable k-CNF formula over n variables has a refutation of size S in the polynomial calculus resolution proof system, then this formula also has a refutation of degree k + O(√(n log S)). The proof of this works by converting a small-size refutation into a small-degree one, but at the expense of increasing the proof size exponentially. This raises the question of whether it is possible to achieve both small size and small degree in the same refutation, or whether the exponential blow-up is inherent. Using and extending ideas from [Thapen '16], who studied the analogous question for the resolution proof system, we prove that a strong size-degree trade-off is necessary.

Cite As Get BibTex

Guillaume Lagarde, Jakob Nordström, Dmitry Sokolov, and Joseph Swernofsky. Trade-Offs Between Size and Degree in Polynomial Calculus. In 11th Innovations in Theoretical Computer Science Conference (ITCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 151, pp. 72:1-72:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020) https://doi.org/10.4230/LIPIcs.ITCS.2020.72

Author Details

Guillaume Lagarde
  • LaBRI, Bordeaux, France
Jakob Nordström
  • University of Copenhagen, Denmark
  • KTH Royal Institute of Technology, Stockholm, Sweden
Dmitry Sokolov
  • Lund University, Sweden
  • University of Copenhagen, Denmark
Joseph Swernofsky
  • KTH Royal Institute of Technology, Stockholm, Sweden

Acknowledgements

The first, second, and fourth authors were funded by the Knut and Alice Wallenberg grant KAW 2016.0066 and the third author by the Knut and Alice Wallenberg grant KAW 2016.0433. In addition, the second author was supported by the Swedish Research Council grants 621-2012-5645 and 2016-00782.

References

  1. Michael Alekhnovich, Eli Ben-Sasson, Alexander A. Razborov, and Avi Wigderson. Space Complexity in Propositional Calculus. SIAM J. Comput., 31(4):1184-1211, 2002. URL: https://doi.org/10.1137/S0097539700366735.
  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 in FOCS '01.
  3. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. J. Comput. Syst. Sci., 74(3):323-334, 2008. URL: https://doi.org/10.1016/j.jcss.2007.06.025.
  4. Albert Atserias and Tuomas Hakoniemi. Size-Degree Trade-Offs for Sums-of-Squares and Positivstellensatz Proofs. In 34th Computational Complexity Conference, CCC 2019, July 18-20, 2019, New Brunswick, NJ, USA., pages 24:1-24:20, 2019. URL: https://doi.org/10.4230/LIPIcs.CCC.2019.24.
  5. Paul Beame, Chris Beck, and Russell Impagliazzo. Time-Space Tradeoffs in Resolution: Superpolynomial Lower Bounds for Superlinear Space. SIAM Journal on Computing, 45(4):1612-1645, August 2016. Preliminary version in STOC '12. URL: https://doi.org/10.1137/130914085.
  6. Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. Lower Bounds on Hilbert’s Nullstellensatz and Propositional Proofs. Proceedings of the London Mathematical Society, s3-73(1):1-26, 1996. URL: https://doi.org/10.1112/plms/s3-73.1.1.
  7. Chris Beck, Jakob Nordström, and Bangsheng Tang. Some Trade-off Results for Polynomial Calculus. In Proceedings of the 45th Annual ACM Symposium on Theory of Computing (STOC '13), pages 813-822, May 2013. URL: https://doi.org/10.1145/2488608.2488711.
  8. Eli Ben-Sasson. Size Space Tradeoffs for Resolution. In Proceedings of the 34th Annual ACM Symposium on Theory of Computing (STOC '02), pages 457-464, May 2002. URL: https://doi.org/10.1145/509907.509975.
  9. Eli Ben-Sasson and Jakob Nordström. Understanding Space in Proof Complexity: Separations and Trade-offs via Substitutions. In Proceedings of the 2nd Symposium on Innovations in Computer Science (ICS '11), pages 401-416, January 2011. URL: http://arxiv.org/abs/1008.1789.
  10. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. URL: https://doi.org/10.1145/375827.375835.
  11. Christoph Berkholz and Jakob Nordström. Supercritical Space-Width Trade-offs for Resolution. In Proceedings of the 43rd International Colloquium on Automata, Languages and Programming (ICALP '16), volume 55 of Leibniz International Proceedings in Informatics (LIPIcs), pages 57:1-57:14, July 2016. URL: https://doi.org/10.4230/LIPIcs.ICALP.2016.57.
  12. Archie Blake. Canonical Expressions in Boolean Algebra. PhD thesis, University of Chicago, 1937. URL: https://doi.org/10.2307/2267634.
  13. María Luisa Bonet and Nicola Galesi. Optimality of Size-Width Tradeoffs for Resolution. Computational Complexity, 10(4):261-276, December 2001. Preliminary version in FOCS '99. URL: https://doi.org/10.1007/s000370100000.
  14. Sam Buss and Jakob Nordström. Proof Complexity and SAT Solving. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability. IOS Press, 2020. Chapter to appear in the 2nd edition. Draft version available at URL: https://www.math.ucsd.edu/~sbuss/ResearchWeb/ProofComplexitySAT/ProofComplexityChapter.pdf.
  15. Matthew Clegg, Jeff Edmonds, and Russell Impagliazzo. Using the Groebner Basis Algorithm to Find Proofs of Unsatisfiability. In Proceedings of the Twenty-Eighth Annual ACM Symposium on the Theory of Computing, Philadelphia, Pennsylvania, USA, May 22-24, 1996, pages 174-183, 1996. URL: https://doi.org/10.1145/237814.237860.
  16. William Cook, Collette Rene Coullard, and György Turán. On the Complexity of Cutting-Plane Proofs. Discrete Applied Mathematics, 18(1):25-38, November 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  17. Susanna F. de Rezende, Jakob Nordström, Or Meir, and Robert Robere. Nullstellensatz size-degree trade-offs from reversible pebbling. In 34th Computational Complexity Conference, CCC 2019, July 18-20, 2019, New Brunswick, NJ, USA., pages 18:1-18:16, 2019. URL: https://doi.org/10.4230/LIPIcs.CCC.2019.18.
  18. Susanna F. de Rezende, Jakob Nordström, and Marc Vinyals. How Limited Interaction Hinders Real Communication (and What It Means for Proof and Circuit Complexity). In Proceedings of the 57th Annual IEEE Symposium on Foundations of Computer Science (FOCS '16), pages 295-304, October 2016. URL: https://doi.org/10.1109/FOCS.2016.40.
  19. Nicola Galesi, Leszek Aleksander Kolodziejczyk, and Neil Thapen. Polynomial calculus space and resolution width. Electronic Colloquium on Computational Complexity (ECCC), 26:52, 2019. URL: https://eccc.weizmann.ac.il/report/2019/052.
  20. Nicola Galesi and Massimo Lauria. On the Automatizability of Polynomial Calculus. Theory of Computing Systems, 47(2):491-506, August 2010. URL: https://doi.org/10.1007/s00224-009-9195-5.
  21. Nicola Galesi and Massimo Lauria. Optimality of Size-Degree Trade-offs for Polynomial Calculus. ACM Transactions on Computational Logic, 12(1):4:1-4:22, November 2010. URL: https://doi.org/10.1.1.703.6976.
  22. Mika Göös and Toniann Pitassi. Communication Lower Bounds via Critical Block Sensitivity. SIAM J. Comput., 47(5):1778-1806, 2018. URL: https://doi.org/10.1137/16M1082007.
  23. Trinh Huynh and Jakob Nordström. On the Virtue of Succinct Proofs: Amplifying Communication Complexity Hardness to Time-Space Trade-offs in Proof Complexity. In Proceedings of the 44th Symposium on Theory of Computing Conference, STOC 2012, New York, NY, USA, May 19 - 22, 2012, pages 233-248, 2012. URL: https://doi.org/10.1145/2213977.2214000.
  24. Russell Impagliazzo, Pavel Pudlák, and Jirí Sgall. Lower Bounds for the Polynomial Calculus and the Gröbner Basis Algorithm. Computational Complexity, 8(2):127-144, 1999. URL: https://doi.org/10.1007/s000370050024.
  25. Jan Krajíček. Proof Complexity, volume 170 of Encyclopedia of Mathematics and Its Applications. Cambridge University Press, March 2019. URL: https://doi.org/10.1017/9781108242066.
  26. Mladen Mikša and Jakob Nordström. A Generalized Method for Proving Polynomial Calculus Degree Lower Bounds. In 30th Conference on Computational Complexity, CCC 2015, June 17-19, 2015, Portland, Oregon, USA, pages 467-487, 2015. URL: https://doi.org/10.4230/LIPIcs.CCC.2015.467.
  27. Jakob Nordström. A Simplified Way of Proving Trade-off Results for Resolution. Information Processing Letters, 109(18):1030-1035, August 2009. Preliminary version in ECCC report TR07-114, 2007. URL: https://doi.org/10.1016/j.ipl.2009.06.006.
  28. Alexander A. Razborov. A New Kind of Tradeoffs in Propositional Proof Complexity. J. ACM, 63(2):16:1-16:14, 2016. URL: https://doi.org/10.1145/2858790.
  29. Neil Thapen. A Tradeoff Between Length and Width in Resolution. Theory of Computing, 12(1):1-14, 2016. URL: https://doi.org/10.4086/toc.2016.v012a005.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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