Document Open Access Logo

Colourful TFNP and Propositional Proofs

Authors Ben Davis, Robert Robere

PDF
Thumbnail PDF

File

LIPIcs.CCC.2023.36.pdf
  • Filesize: 0.8 MB
  • 21 pages

Document Identifiers

Author Details

Ben Davis
  • School of Computer Science, McGill University, Montreal, Canada
Robert Robere
  • School of Computer Science, McGill University, Montreal, Canada

Funding

B.D. and R.R. supported by NSERC.

Cite As Get BibTex

Ben Davis and Robert Robere. Colourful TFNP and Propositional Proofs. In 38th Computational Complexity Conference (CCC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 264, pp. 36:1-36:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CCC.2023.36

Abstract

Recent work has shown that many of the standard TFNP classes - such as PLS, PPADS, PPAD, SOPL, and EOPL - have corresponding proof systems in propositional proof complexity, in the sense that a total search problem is in the class if and only if the totality of the problem can be efficiently proved by the corresponding proof system. We build on this line of work by studying coloured variants of these TFNP classes: C-PLS, C-PPADS, C-PPAD, C-SOPL, and C-EOPL. While C-PLS has been studied in the literature before, the coloured variants of the other classes are introduced here for the first time. We give a family of results showing that these coloured TFNP classes are natural objects of study, and that the correspondence between TFNP and natural propositional proof systems is not an exceptional phenomenon isolated to weak TFNP classes. Namely, we show that:  
- Each of the classes C-PLS, C-PPADS, and C-SOPL have corresponding proof systems characterizing them. Specifically, the proof systems for these classes are obtained by adding depth to the formulas in the corresponding proof system for the uncoloured class. For instance, while it was previously known that PLS is characterized by bounded-width Resolution (i.e. depth 0.5 Frege), we prove that C-PLS is characterized by depth-1.5 Frege (Res(polylog(n)). 
- The classes C-PPAD and C-EOPL coincide exactly with the uncoloured classes PPADS and SOPL, respectively. Thus, both of these classes also have corresponding proof systems: unary Sherali-Adams and Reversible Resolution, respectively. 
- Finally, we prove a coloured intersection theorem for the coloured sink classes, showing C-PLS ∩ C-PPADS = C-SOPL, generalizing the intersection theorem PLS ∩ PPADS = SOPL. However, while it is known in the uncoloured world that PLS ∩ PPAD = EOPL = CLS, we prove that this equality fails in the coloured world in the black-box setting. More precisely, we show that there is an oracle O such that C-PLS^O ∩ C-PPAD^O ⊋ C-EOPL^O.  To prove our results, we introduce an abstract multivalued proof system - the Blockwise Calculus - which may be of independent interest.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • oracle separations
  • TFNP
  • proof complexity
  • Res(k)
  • lower bounds

Metrics

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

Related Versions

References

  1. Albert Atserias and Maria Luisa Bonet. On the automatizability of resolution and related propositional proof systems. Inf. Comput., 189(2):182-201, 2004. URL: https://doi.org/10.1016/j.ic.2003.10.004.
  2. Albert Atserias and Massimo Lauria. Circular (yet sound) proofs. In Proceedings of the 22nd Theory and Applications of Satisfiability Testing (SAT), pages 1-18. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_1.
  3. Paul Beame, Stephen Cook, Jeff Edmonds, Russell Impagliazzo, and Toniann Pitassi. The relative complexity of NP search problems. Journal of Computer and System Sciences, 57(1):3-19, 1998. URL: https://doi.org/10.1006/jcss.1998.1575.
  4. Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák. Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. In Proceedings of the 35th Symposium on Foundations of Computer Science (FOCS), pages 794-806, 1994. URL: https://doi.org/10.1109/SFCS.1994.365714.
  5. Arnold Beckmann and Samuel R. Buss. Characterising definable search problems in bounded arithmetic via proof notations. In Ways of Proof Theory, ONTOS Series in Mathematical Logic, pages 65-134, 2010. Google Scholar
  6. Ilario Bonacina and Maria Luisa Bonet. On the strength of sherali-adams and nullstellensatz as propositional proof systems. In Christel Baier and Dana Fisman, editors, LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Haifa, Israel, August 2 - 5, 2022, pages 25:1-25:12. ACM, 2022. URL: https://doi.org/10.1145/3531130.3533344.
  7. María Luisa Bonet, Jordi Levy, and Felip Manyà. Resolution for Max-SAT. Artificial Intelligence, 171(8-9):606-618, 2007. URL: https://doi.org/10.1016/j.artint.2007.03.001.
  8. Joshua Buresh-Oppenheim and Tsuyoshi Morioka. Relativized NP search problems and propositional proof systems. In Proceedings of the 19th IEEE Conference on Computational Complexity (CCC), pages 54-67, 2004. URL: https://doi.org/10.1109/CCC.2004.1313795.
  9. Sam Buss, Noah Fleming, and Russell Impagliazzo. Tfnp characterizations of proof systems and monotone circuits. Electron. Colloquium Comput. Complex., TR22-141, 2022. URL: https://arxiv.org/abs/TR22-141.
  10. Samuel R. Buss and Alan S. Johnson. Propositional proofs and reductions between NP search problems. Annals of Pure and Applied Logic, 163(9):1163-1182, 2012. URL: https://doi.org/10.1016/j.apal.2012.01.015.
  11. Xi Chen, Decheng Dai, Ye Du, and Shang-Hua Teng. Settling the complexity of Arrow-Debreu equilibria in markets with additively separable utilities. In Proceedings of the 50th Symposium on Foundations of Computer Science (FOCS), pages 273-282, 2009. URL: https://doi.org/10.1109/FOCS.2009.29.
  12. Xi Chen, Dimitris Paparas, and Mihalis Yannakakis. The complexity of non-monotone markets. Journal of the ACM, 64(3):20:1-20:56, 2017. URL: https://doi.org/10.1145/3064810.
  13. Bruno Codenotti, Amin Saberi, Kasturi Varadarajan, and Yinyu Ye. The complexity of equilibria: Hardness results for economies via a correspondence with games. Theoretical Computer Science, 408(2-3):188-198, 2008. URL: https://doi.org/10.1016/j.tcs.2008.08.007.
  14. Stefan S. Dantchev, Barnaby Martin, and Mark Nicholas Charles Rhodes. Tight rank lower bounds for the sherali-adams proof system. Theor. Comput. Sci., 410(21-23):2054-2063, 2009. URL: https://doi.org/10.1016/j.tcs.2009.01.002.
  15. Constantinos Daskalakis, Paul Goldberg, and Christos Papadimitriou. The complexity of computing a Nash equilibrium. SIAM Journal on Computing, 39(1):195-259, 2009. URL: https://doi.org/10.1137/070699652.
  16. John Fearnley, Paul W. Goldberg, Alexandros Hollender, and Rahul Savani. The complexity of gradient descent: CLS = PPAD ∩ PLS. In Proceedings of the 53rd Symposium on Theory of Computing (STOC), pages 46-59, 2021. URL: https://doi.org/10.1145/3406325.3451052.
  17. Yuval Filmus, Meena Mahajan, Gaurav Sood, and Marc Vinyals. MaxSAT resolution and subcube sums. In Proceedings of the 23rd Theory and Applications of Satisfiability Testing (SAT), pages 295-311. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_21.
  18. Michal Garlík. Failure of feasible disjunction property for k-dnf resolution and np-hardness of automating it. CoRR, abs/2003.10230, 2020. URL: https://arxiv.org/abs/2003.10230.
  19. Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Further collapses in TFNP. In Proceedings of the 37th Computational Complexity Conference (CCC), pages 33:1-33:15, 2022. URL: https://doi.org/10.4230/LIPICS.CCC.2022.33.
  20. Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Separations in proof complexity and TFNP. Electron. Colloquium Comput. Complex., TR22-058, 2022. URL: https://arxiv.org/abs/TR22-058.
  21. Mika Göös, Pritish Kamath, Robert Robere, and Dmitry Sokolov. Adventures in monotone complexity and TFNP. In Proceedings of the 10th Innovations in Theoretical Computer Science Conference (ITCS), volume 124, pages 38:1-38:19, 2018. URL: https://doi.org/10.4230/LIPIcs.ITCS.2019.38.
  22. David Johnson, Christos Papadimitriou, and Mihalis Yannakakis. How easy is local search? Journal of Computer and System Sciences, 37(1):79-100, 1988. URL: https://doi.org/10.1016/0022-0000(88)90046-3.
  23. Jan Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170(1-3):123-140, 2001. Google Scholar
  24. Jan Krajícek, Alan Skelley, and Neil Thapen. NP search problems in low fragments of bounded arithmetic. J. Symb. Log., 72(2):649-672, 2007. URL: https://doi.org/10.2178/jsl/1185803628.
  25. Javier Larrosa, Federico Heras, and Simon de Givry. A logical approach to efficient Max-SAT solving. Artificial Intelligence, 172(2-3):204-233, 2008. URL: https://doi.org/10.1016/j.artint.2007.05.006.
  26. Nimrod Megiddo and Christos Papadimitriou. On total functions, existence theorems and computational complexity. Theoretical Computer Science, 81(2):317-324, 1991. URL: https://doi.org/10.1016/0304-3975(91)90200-L.
  27. Christos Papadimitriou. On the complexity of the parity argument and other inefficient proofs of existence. Journal of Computer and System Sciences, 48(3):498-532, 1994. URL: https://doi.org/10.1016/s0022-0000(05)80063-7.
  28. 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.
  29. Hanif Sherali and Warren Adams. A hierarchy of relaxations and convex hull characterizations for mixed-integer zero-one programming problems. Discrete Applied Mathematics, 52(1):83-106, July 1994. URL: https://doi.org/10.1016/0166-218x(92)00190-w.
  30. Alan Skelley and Neil Thapen. The provably total search problems of bounded arithmetic. Proceedings of the London Mathematical Society, 103(1):106-138, 2011. Google Scholar
  31. Neil Thapen. A tradeoff between length and width in resolution. Theory Comput., 12(1):1-14, 2016. URL: https://doi.org/10.4086/toc.2016.v012a005.
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 About DROPS Imprint Privacy Contact