Document Open Access Logo

TFNP Characterizations of Proof Systems and Monotone Circuits

Authors Sam Buss, Noah Fleming , Russell Impagliazzo

PDF
Thumbnail PDF

File

LIPIcs.ITCS.2023.30.pdf
  • Filesize: 0.97 MB
  • 40 pages

Document Identifiers

Author Details

Sam Buss
  • University of California, San Diego, CA, USA
Noah Fleming
  • Memorial University, St. John’s, Canada
Russell Impagliazzo
  • University of California, San Diego, CA, USA

Funding

  • Fleming, Noah: NSERC.
  • Impagliazzo, Russell: NSF CCF 2212135 and the Simons Foundation.

Cite AsGet BibTex

Sam Buss, Noah Fleming, and Russell Impagliazzo. TFNP Characterizations of Proof Systems and Monotone Circuits. In 14th Innovations in Theoretical Computer Science Conference (ITCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 251, pp. 30:1-30:40, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITCS.2023.30

Abstract

Connections between proof complexity and circuit complexity have become major tools for obtaining lower bounds in both areas. These connections - which take the form of interpolation theorems and query-to-communication lifting theorems - translate efficient proofs into small circuits, and vice versa, allowing tools from one area to be applied to the other. Recently, the theory of TFNP has emerged as a unifying framework underlying these connections. For many of the proof systems which admit such a connection there is a TFNP problem which characterizes it: the class of problems which are reducible to this TFNP problem via query-efficient reductions is equivalent to the tautologies that can be efficiently proven in the system. Through this, proof complexity has become a major tool for proving separations in black-box TFNP. Similarly, for certain monotone circuit models, the class of functions that it can compute efficiently is equivalent to what can be reduced to a certain TFNP problem in a communication-efficient manner. When a TFNP problem has both a proof and circuit characterization, one can prove an interpolation theorem. Conversely, many lifting theorems can be viewed as relating the communication and query reductions to TFNP problems. This is exciting, as it suggests that TFNP provides a roadmap for the development of further interpolation theorems and lifting theorems. In this paper we begin to develop a more systematic understanding of when these connections to TFNP occur. We give exact conditions under which a proof system or circuit model admits a characterization by a TFNP problem. We show: - Every well-behaved proof system which can prove its own soundness (a reflection principle) is characterized by a TFNP problem. Conversely, every TFNP problem gives rise to a well-behaved proof system which proves its own soundness. - Every well-behaved monotone circuit model which admits a universal family of functions is characterized by a TFNP problem. Conversely, every TFNP problem gives rise to a well-behaved monotone circuit model with a universal problem. As an example, we provide a TFNP characterization of the Polynomial Calculus, answering a question from [Mika Göös et al., 2022], and show that it can prove its own soundness.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof Complexity
  • Circuit Complexity
  • TFNP

Metrics

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

References

  1. Albert Atserias and Moritz Müller. Automating resolution is NP-hard. Journal of the Association for Computing Machinery, 67(5):31:1-31:17, 2020. Google Scholar
  2. 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.
  3. Paul Beame, Stephen A. Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi. The relative complexity of NP search problems. J. Comput. Syst. Sci., 57(1):3-19, 1998. URL: https://doi.org/10.1006/jcss.1998.1575.
  4. Arnold Beckmann and Sam Buss. The NP search problems of frege and extended frege proofs. ACM Trans. Comput. Log., 18(2):11:1-11:19, 2017. URL: https://doi.org/10.1145/3060145.
  5. Arnold Beckmann and Samuel R. Buss. The NP search problems of Frege and extended Frege proofs. ACM Transactions on Computational Logic, 18(2):Article 11, 2017. Google Scholar
  6. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. Lower bounds for cutting planes proofs with small coefficients. J. Symb. Log., 62(3):708-728, 1997. URL: https://doi.org/10.2307/2275569.
  7. Josh Buresh-Oppenheim and Tsuyoshi Morioka. Relativized NP search problems and propositional proof systems. In 19th Annual IEEE Conference on Computational Complexity (CCC 2004), 21-24 June 2004, Amherst, MA, USA, pages 54-67. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/CCC.2004.1313795.
  8. Samuel R. Buss. The Boolean formula value problem is in ALOGTIME. In Proceedings of the 19-th Annual ACM Symposium on Theory of Computing, pages 123-131, May 1987. Google Scholar
  9. Samuel R. Buss, Leszek Aleksander Kolodziejczyk, and Neil Thapen. Fragments of approximate counting. J. Symb. Log., 79(2):496-525, 2014. URL: https://doi.org/10.1017/jsl.2013.37.
  10. Siu On Chan, James R. Lee, Prasad Raghavendra, and David Steurer. Approximate constraint satisfaction requires large LP relaxations. J. ACM, 63(4):34:1-34:22, 2016. URL: https://doi.org/10.1145/2811255.
  11. Stephen A. Cook. Feasibly constructive proofs and the propositional calculus. In Proceedings of the Seventh Annual ACM Symposium on Theory of Computing, pages 83-97. Association for Computing Machinery, 1975. Google Scholar
  12. Susanna F. de Rezende, Mika Göös, and Robert Robere. Guest column: Proofs, circuits, and communication. SIGACT News, 53(1):59-82, 2022. URL: https://doi.org/10.1145/3532737.3532746.
  13. Susanna F. de Rezende, Massimo Lauria, Jakob Nordström, and Dmitry Sokolov. The power of negative reasoning. In Valentine Kabanets, editor, 36th Computational Complexity Conference, CCC 2021, July 20-23, 2021, Toronto, Ontario, Canada (Virtual Conference), volume 200 of LIPIcs, pages 40:1-40:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CCC.2021.40.
  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 Sandy Irani, editor, 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. 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). Electron. Colloquium Comput. Complex., page 6, 2021. URL: https://eccc.weizmann.ac.il/report/2021/006, URL: http://arxiv.org/abs/TR21-006.
  16. Noah Fleming. The Proof Complexity of Integer Programming. PhD thesis, University of Toronto, Canada, 2021. URL: http://hdl.handle.net/1807/108797.
  17. Noah Fleming, Mika Göös, Stefan Grosser, and Robert Robere. On semi-algebraic proofs and algorithms. In Mark Braverman, editor, 13th Innovations in Theoretical Computer Science Conference, ITCS 2022, January 31 - February 3, 2022, Berkeley, CA, USA, volume 215 of LIPIcs, pages 69:1-69:25. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ITCS.2022.69.
  18. Noah Fleming, Pravesh Kothari, and Toniann Pitassi. Semialgebraic proofs and efficient algorithm design. Found. Trends Theor. Comput. Sci., 14(1-2):1-221, 2019. URL: https://doi.org/10.1561/0400000086.
  19. Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random Θ(log n)-CNFs are hard for cutting planes. J. ACM, 69(3):19:1-19:32, 2022. URL: https://doi.org/10.1145/3486680.
  20. Anna Gál. A characterization of span program size and improved lower bounds for monotone span programs. Comput. Complex., 10(4):277-296, 2001. URL: https://doi.org/10.1007/s000370100001.
  21. 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.
  22. Michal Garlik. Resolution lower bounds for refutation statements. In Proc. 4 Intl. Symp. on Mathematical Foundations of Computer Science (MFCS), pages 37:1-37:13, 2019. Google Scholar
  23. Paul Goldberg and Christos Papadimitriou. Towards a unified complexity theory of total functions. Journal of Computer and System Sciences, 94:167-192, 2018. Google Scholar
  24. Paul W. Goldberg and Christos H. Papadimitriou. Towards a unified complexity theory of total functions. Electron. Colloquium Comput. Complex., page 56, 2017. URL: https://eccc.weizmann.ac.il/report/2017/056, URL: http://arxiv.org/abs/TR17-056.
  25. Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Separations in proof complexity and TFNP. CoRR, abs/2205.02168, 2022. URL: https://doi.org/10.48550/arXiv.2205.02168.
  26. Mika Göös, Pritish Kamath, Robert Robere, and Dmitry Sokolov. Adventures in monotone complexity and TFNP. In Avrim Blum, editor, 10th Innovations in Theoretical Computer Science Conference, ITCS 2019, January 10-12, 2019, San Diego, California, USA, volume 124 of LIPIcs, pages 38:1-38:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITCS.2019.38.
  27. Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi. Automating cutting planes is NP-hard. In Konstantin Makarychev, Yury Makarychev, Madhur Tulsiani, Gautam Kamath, and Julia Chuzhoy, editors, Proccedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, Chicago, IL, USA, June 22-26, 2020, pages 68-77. ACM, 2020. URL: https://doi.org/10.1145/3357713.3384248.
  28. Mika Göös, Shachar Lovett, Raghu Meka, Thomas Watson, and David Zuckerman. Rectangles are nonnegative juntas. SIAM J. Comput., 45(5):1835-1869, 2016. URL: https://doi.org/10.1137/15M103145X.
  29. Mika Göös, Toniann Pitassi, and Thomas Watson. Deterministic communication vs. partition number. SIAM J. Comput., 47(6):2435-2450, 2018. URL: https://doi.org/10.1137/16M1059369.
  30. 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.
  31. Pritish Kamath. Some hardness escalation results in computational complexity theory. PhD thesis, Massachusetts Institute of Technology, 2019. Google Scholar
  32. Mauricio Karchmer and Avi Wigderson. Monotone circuits for connectivity require super-logarithmic depth. SIAM J. Discret. Math., 3(2):255-265, 1990. URL: https://doi.org/10.1137/0403021.
  33. Pravesh K. Kothari, Raghu Meka, and Prasad Raghavendra. Approximating rectangles by juntas and weakly-exponential lower bounds for LP relaxations of CSPs. In Hamed Hatami, Pierre McKenzie, and Valerie King, editors, Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2017, Montreal, QC, Canada, June 19-23, 2017, pages 590-603. ACM, 2017. URL: https://doi.org/10.1145/3055399.3055438.
  34. Jan Krajícek. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log., 62(2):457-486, 1997. URL: https://doi.org/10.2307/2275541.
  35. Jan Krajícek. Interpolation by a game. Math. Log. Q., 44:450-458, 1998. URL: https://doi.org/10.1002/malq.19980440403.
  36. Jan Krajícek. Randomized feasible interpolation and monotone circuits with a local oracle. J. Math. Log., 18(2):1850012:1-1850012:27, 2018. URL: https://doi.org/10.1142/S0219061318500125.
  37. James R. Lee, Prasad Raghavendra, and David Steurer. Lower bounds on the size of semidefinite programming relaxations. In Rocco A. Servedio and Ronitt Rubinfeld, editors, Proceedings of the Forty-Seventh Annual ACM on Symposium on Theory of Computing, STOC 2015, Portland, OR, USA, June 14-17, 2015, pages 567-576. ACM, 2015. URL: https://doi.org/10.1145/2746539.2746599.
  38. László Lovász, Moni Naor, Ilan Newman, and Avi Wigderson. Search problems in the decision tree model. SIAM J. Discret. Math., 8(1):119-132, 1995. URL: https://doi.org/10.1137/S0895480192233867.
  39. Shachar Lovett, Raghu Meka, Ian Mertz, Toniann Pitassi, and Jiapeng Zhang. Lifting with sunflowers. In Mark Braverman, editor, 13th Innovations in Theoretical Computer Science Conference, ITCS 2022, January 31 - February 3, 2022, Berkeley, CA, USA, volume 215 of LIPIcs, pages 104:1-104:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ITCS.2022.104.
  40. Toniann Pitassi and Robert Robere. Lifting nullstellensatz to monotone span programs over any field. 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 1207-1219. ACM, 2018. URL: https://doi.org/10.1145/3188745.3188914.
  41. 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.
  42. Pavel Pudlák. On the complexity of finding falsifying assignments for herbrand disjunctions. Arch. Math. Log., 54(7-8):769-783, 2015. URL: https://doi.org/10.1007/s00153-015-0439-6.
  43. Pavel Pudlák and Jirí Sgall. Algebraic models of computation and interpolation for algebraic proof systems. In Paul Beame and Samuel R. Buss, editors, Proof Complexity and Feasible Arithmetics, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, April 21-24, 1996, volume 39 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 279-295. DIMACS/AMS, 1996. URL: https://doi.org/10.1090/dimacs/039/15.
  44. Ran Raz and Pierre McKenzie. Separation of the monotone NC hierarchy. Comb., 19(3):403-435, 1999. URL: https://doi.org/10.1007/s004930050062.
  45. Alexander Razborov. Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic. Izvestiya Mathematics, 59(1):205-227, 1995. Google Scholar
  46. Robert Robere. Separations in proof complexity and TFNP. Talk at the Satisfiability: Theory, Practice, and Beyond Reunion, Simons Institute, Berkeley, 2022. Google Scholar
  47. Robert Robere, Toniann Pitassi, Benjamin Rossman, and Stephen A. Cook. Exponential lower bounds for monotone span programs. In Irit Dinur, editor, IEEE 57th Annual Symposium on Foundations of Computer Science, FOCS 2016, 9-11 October 2016, Hyatt Regency, New Brunswick, New Jersey, USA, pages 406-415. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/FOCS.2016.51.
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