Document Open Access Logo

Extremely Deep Proofs

Authors Noah Fleming, Toniann Pitassi, Robert Robere

PDF
Thumbnail PDF

File

LIPIcs.ITCS.2022.70.pdf
  • Filesize: 0.75 MB
  • 23 pages

Document Identifiers

Author Details

Noah Fleming
  • University of California, San Diego, CA, USA
  • Memorial University, Canada
Toniann Pitassi
  • University of Toronto, Canada
  • Columbia University, New York, NY, USA
  • IAS, Princeton, NJ, USA
Robert Robere
  • McGill University, Montreal, Canada

Funding

  • Fleming, Noah: Research supported by NSERC.
  • Pitassi, Toniann: Research supported by NSERC, the IAS School of Mathematics and NSF Grant No. CCF-1900460.
  • Robere, Robert: Research supported by NSERC.

Cite AsGet BibTex

Noah Fleming, Toniann Pitassi, and Robert Robere. Extremely Deep Proofs. In 13th Innovations in Theoretical Computer Science Conference (ITCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 215, pp. 70:1-70:23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ITCS.2022.70

Abstract

We further the study of supercritical tradeoffs in proof and circuit complexity, which is a type of tradeoff between complexity parameters where restricting one complexity parameter forces another to exceed its worst-case upper bound. In particular, we prove a new family of supercritical tradeoffs between depth and size for Resolution, Res(k), and Cutting Planes proofs. For each of these proof systems we construct, for each c ≤ n^{1-ε}, a formula with n^{O(c)} clauses and n variables that has a proof of size n^{O(c)} but in which any proof of size no more than roughly exponential in n^{1-ε}/c must necessarily have depth ≈ n^c. By setting c = o(n^{1-ε}) we therefore obtain exponential lower bounds on proof depth; this far exceeds the trivial worst-case upper bound of n. In doing so we give a simplified proof of a supercritical depth/width tradeoff for tree-like Resolution from [Alexander A. Razborov, 2016]. Finally, we outline several conjectures that would imply similar supercritical tradeoffs between size and depth in circuit complexity via lifting theorems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof Complexity
  • Tradeoffs
  • Resolution
  • Cutting Planes

Metrics

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

References

  1. Karen Aardal, Robert E. Bixby, Cor A. J. Hurkens, Arjen K. Lenstra, and Job W. Smeltink. Market split and basis reduction: Towards a solution of the cornuéjols-dawande instances. INFORMS J. Comput., 12(3):192-202, 2000. URL: https://doi.org/10.1287/ijoc.12.3.192.12635.
  2. Michael Alekhnovich. Lower bounds for k-DNF resolution on random 3-CNFs. In Harold N. Gabow and Ronald Fagin, editors, Proceedings of the 37th Annual ACM Symposium on Theory of Computing, Baltimore, MD, USA, May 22-24, 2005, pages 251-256. ACM, 2005. URL: https://doi.org/10.1145/1060590.1060628.
  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. Paul Beame, Chris Beck, and Russell Impagliazzo. Time-space trade-offs in resolution: Superpolynomial lower bounds for superlinear space. SIAM J. Comput., 45(4):1612-1645, 2016. URL: https://doi.org/10.1137/130914085.
  5. Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing planes. In 9th Innovations in Theoretical Computer Science Conference, ITCS 2018, January 11-14, 2018, Cambridge, MA, USA, pages 10:1-10:20, 2018. URL: https://doi.org/10.4230/LIPIcs.ITCS.2018.10.
  6. Chris Beck, Jakob Nordström, and Bangsheng Tang. Some trade-off results for polynomial calculus: extended abstract. In Dan Boneh, Tim Roughgarden, and Joan Feigenbaum, editors, Symposium on Theory of Computing Conference, STOC'13, Palo Alto, CA, USA, June 1-4, 2013, pages 813-822. ACM, 2013. URL: https://doi.org/10.1145/2488608.2488711.
  7. 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.
  8. Christoph Berkholz. On the complexity of finding narrow proofs. In 53rd Annual IEEE Symposium on Foundations of Computer Science, FOCS 2012, New Brunswick, NJ, USA, October 20-23, 2012, pages 351-360. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/FOCS.2012.48.
  9. Christoph Berkholz and Jakob Nordström. Supercritical space-width trade-offs for resolution. SIAM J. Comput., 49(1):98-118, 2020. URL: https://doi.org/10.1137/16M1109072.
  10. Joshua Buresh-Oppenheim, Nicola Galesi, Shlomo Hoory, Avner Magen, and Toniann Pitassi. Rank bounds and integrality gaps for cutting planes procedures. Theory of Computing, 2(4):65-90, 2006. URL: https://doi.org/10.4086/toc.2006.v002a004.
  11. Siu Man Chan. Just a pebble game. In Proceedings of the 28th Conference on Computational Complexity, CCC 2013, K.lo Alto, California, USA, 5-7 June, 2013, pages 133-143. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/CCC.2013.22.
  12. Vašek Chvátal, William Cook, and Mark Hartmann. On cutting-plane proofs in combinatorial optimization. Linear algebra and its applications, 114:455-499, 1989. Google Scholar
  13. Daniel Dadush and Samarth Tiwari. On the complexity of branching proofs. In Shubhangi Saraf, editor, 35th Computational Complexity Conference, CCC 2020, July 28-31, 2020, Saarbrücken, Germany (Virtual Conference), volume 169 of LIPIcs, pages 34:1-34:35. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CCC.2020.34.
  14. Susanna F. de Rezende, Or Meir, Jakob Nordström, Toniann Pitassi, Robert Robere, and Marc Vinyals. Lifting with simple gadgets and applications to circuit and proof complexity. In 61st IEEE Annual Symposium on Foundations of Computer Science, FOCS 2020, Durham, NC, USA, November 16-19, 2020, pages 24-30. IEEE, 2020. URL: https://doi.org/10.1109/FOCS46700.2020.00011.
  15. Friedrich Eisenbrand and Andreas S. Schulz. Bounds on the chvátal rank of polytopes in the 0/1-cube. In Gérard Cornuéjols, Rainer E. Burkard, and Gerhard J. Woeginger, editors, Integer Programming and Combinatorial Optimization, 7th International IPCO Conference, Graz, Austria, June 9-11, 1999, Proceedings, volume 1610 of Lecture Notes in Computer Science, pages 137-150. Springer, 1999. URL: https://doi.org/10.1007/3-540-48777-8_11.
  16. Juan Luis Esteban and Jacobo Torán. A combinatorial characterization of treelike resolution space. Inf. Process. Lett., 87(6):295-300, 2003. URL: https://doi.org/10.1016/S0020-0190(03)00345-4.
  17. Yuval Filmus, Pavel Hrubeš, and Massimo Lauria. Semantic versus syntactic cutting planes. In Nicolas Ollinger and Heribert Vollmer, editors, 33rd Symposium on Theoretical Aspects of Computer Science, STACS 2016, February 17-20, 2016, Orléans, France, volume 47 of LIPIcs, pages 35:1-35:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.STACS.2016.35.
  18. Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson. On the power and limitations of branch and cut. In Valentine Kabanets, editor, 36th Computational Complexity Conference, CCC 2021, July 20-23, 2021, Toronto, Ontario, Canada (Virtual Conference), volume 200 of LIPIcs, pages 6:1-6:30. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CCC.2021.6.
  19. Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random Θ(log n)-CNFs are hard for cutting planes. In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 109-120, 2017. URL: https://doi.org/10.1109/FOCS.2017.19.
  20. Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds from 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 902-911. ACM, 2018. URL: https://doi.org/10.1145/3188745.3188838.
  21. 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.
  22. Pavel Hrubeš and Pavel Pudlák. Random formulas, monotone circuits, and interpolation. In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 121-131, 2017. URL: https://doi.org/10.1109/FOCS.2017.20.
  23. Shachar Lovett, Raghu Meka, Ian Mertz, Toniann Pitassi, and Jiapeng Zhang. Lifting with sunflowers. unpublished. Google Scholar
  24. Shachar Lovett, Raghu Meka, Ian Mertz, Toniann Pitassi, and Jiapeng Zhang. Lifting with sunflowers. In Electron. Colloquium Comput. Complex, page 111, 2020. Google Scholar
  25. Theodoros Papamakarios and Alexander A. Razborov. Space characterizations of complexity measures and size-space trade-offs in propositional proof systems. Electron. Colloquium Comput. Complex., 28:74, 2021. URL: https://eccc.weizmann.ac.il/report/2021/074.
  26. Wolfgang J. Paul, Robert Endre Tarjan, and James R. Celoni. Space bounds for a game on graphs. Math. Syst. Theory, 10:239-251, 1977. URL: https://doi.org/10.1007/BF01683275.
  27. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log., 62(3):981-998, 1997. URL: https://doi.org/10.2307/2275583.
  28. Pavel Pudlák. Proofs as games. Am. Math. Mon., 107(6):541-550, 2000. URL: http://www.jstor.org/stable/2589349.
  29. Ran Raz and Avi Wigderson. Monotone circuits for matching require linear depth. J. ACM, 39(3):736-744, 1992. URL: https://doi.org/10.1145/146637.146684.
  30. Alexander A. Razborov. Lower bounds on monotone complexity of the logical permanent. Mathematical Notes of the Academy of Sciences of the USSR, 37(6):485-493, 1985. Google Scholar
  31. 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.
  32. Alexander A. Razborov. On the width of semialgebraic proofs and algorithms. Math. Oper. Res., 42(4):1106-1134, 2017. URL: https://doi.org/10.1287/moor.2016.0840.
  33. Alexander A. Razborov. On space and depth in resolution. Comput. Complex., 27(3):511-559, 2018. URL: https://doi.org/10.1007/s00037-017-0163-1.
  34. Thomas Rothvoß and Laura Sanita. 0/1 polytopes with quadratic chvátal rank. In International Conference on Integer Programming and Combinatorial Optimization, pages 349-361. Springer, 2013. Google Scholar
  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.
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 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact