Intersection Classes in TFNP and Proof Complexity

Authors Yuhao Li, William Pires, Robert Robere

Thumbnail PDF


  • Filesize: 0.93 MB
  • 22 pages

Document Identifiers

Author Details

Yuhao Li
  • Columbia University, New York, NY, USA
William Pires
  • Columbia University, New York, NY, USA
Robert Robere
  • McGill University, Montreal, Canada


Part of this work was done while the authors were visiting the Simons Institute for the Theory of Computing at UC Berkeley.

Cite AsGet BibTex

Yuhao Li, William Pires, and Robert Robere. Intersection Classes in TFNP and Proof Complexity. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 74:1-74:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


A recent breakthrough in the theory of total NP search problems (TFNP) by Fearnley, Goldberg, Hollender, and Savani has shown that CLS = PLS ∩ PPAD, or, in other words, the class of problems reducible to gradient descent are exactly those problems in the intersection of the complexity classes PLS and PPAD. Since this result, two more intersection theorems have been discovered in this theory: EOPL = PLS ∩ PPAD and SOPL = PLS ∩ PPADS. It is natural to wonder if this exhausts the list of intersection classes in TFNP, or, if other intersections exist. In this work, we completely classify all intersection classes involved among the classical TFNP classes PLS, PPAD, and PPA, giving new complete problems for the newly-introduced intersections. Following the close links between the theory of TFNP and propositional proof complexity, we develop new proof systems - each of which is a generalization of the classical Resolution proof system - that characterize all of the classes, in the sense that a query total search problem is in the intersection class if and only if a tautology associated with the search problem has a short proof in the proof system. We complement these new characterizations with black-box separations between all of the newly introduced classes and prior classes, thus giving strong evidence that no further collapse occurs. Finally, we characterize arbitrary intersections and joins of the PPA_q classes for q ≥ 2 in terms of the Nullstellensatz proof systems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Complexity classes
  • Theory of computation → Proof complexity
  • Theory of computation → Complexity theory and logic
  • TFNP
  • Proof Complexity
  • Intersection Classes


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


  1. 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:
  2. 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:
  3. Ilario Bonacina and Maria Luisa Bonet. On the strength of sherali-adams and nullstellensatz as propositional proof systems. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '22, New York, NY, USA, 2022. Association for Computing Machinery. URL:
  4. 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:
  5. Sam Buss, Noah Fleming, and Russell Impagliazzo. TFNP characterizations of proof systems and monotone circuits. In Yael Tauman Kalai, editor, 14th Innovations in Theoretical Computer Science Conference, ITCS 2023, January 10-13, 2023, MIT, Cambridge, Massachusetts, USA, volume 251 of LIPIcs, pages 30:1-30:40. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL:
  6. Sam Buss and Jan Krajícek. An application of boolean complexity to separation problems in bounded arithmetic. Proceedings of the London Mathematical Society, 69:1-21, 1994. Google Scholar
  7. Samuel R Buss. Lower bounds on nullstellensatz proofs via designs. Proof complexity and feasible arithmetics, 39:59-71, 1996. Google Scholar
  8. Samuel R. Buss and Alan S. Johnson. Propositional proofs and reductions between NP search problems. Ann. Pure Appl. Log., 163(9):1163-1182, 2012. URL:
  9. Xi Chen, Decheng Dai, Ye Du, and Shang-Hua Teng. Settling the complexity of arrow-debreu equilibria in markets with additively separable utilities. In 50th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2009, October 25-27, 2009, Atlanta, Georgia, USA, pages 273-282. IEEE Computer Society, 2009. URL:
  10. Xi Chen, Xiaotie Deng, and Shang-Hua Teng. Settling the complexity of computing two-player nash equilibria. J. ACM, 56(3):14:1-14:57, 2009. URL:
  11. Xi Chen, David Durfee, and Anthi Orfanou. On the complexity of nash equilibria in anonymous games. 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 381-390. ACM, 2015. URL:
  12. Xi Chen, Dimitris Paparas, and Mihalis Yannakakis. The complexity of non-monotone markets. J. ACM, 64(3):20:1-20:56, 2017. URL:
  13. Bruno Codenotti, Amin Saberi, Kasturi R. Varadarajan, and Yinyu Ye. The complexity of equilibria: Hardness results for economies via a correspondence with games. Theor. Comput. Sci., 408(2-3):188-198, 2008. URL:
  14. Constantinos Daskalakis, Paul W. Goldberg, and Christos H. Papadimitriou. The complexity of computing a nash equilibrium. SIAM J. Comput., 39(1):195-259, 2009. URL:
  15. Ben Davis and Robert Robere. Colourful TFNP and propositional proofs. In Amnon Ta-Shma, editor, 38th Computational Complexity Conference, CCC 2023, July 17-20, 2023, Warwick, UK, volume 264 of LIPIcs, pages 36:1-36:21. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL:
  16. John Fearnley, Paul Goldberg, Alexandros Hollender, and Rahul Savani. The complexity of gradient descent: CLS = PPAD ∩ PLS. J. ACM, 70(1):7:1-7:74, 2023. URL:
  17. John Fearnley, Spencer Gordon, Ruta Mehta, and Rahul Savani. Unique end of potential line. J. Comput. Syst. Sci., 114:1-35, 2020. URL:
  18. Noah Fleming, Pravesh Kothari, and Toniann Pitassi. Semialgebraic proofs and efficient algorithm design. Foundations and Trends in Theoretical Computer Science, 14(1-2):1-221, 2019. URL:
  19. Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Further collapses in TFNP. In Shachar Lovett, editor, 37th Computational Complexity Conference, CCC 2022, July 20-23, 2022, Philadelphia, PA, USA, volume 234 of LIPIcs, pages 33:1-33:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL:
  20. Mika Göös, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre, William Pires, Robert Robere, and Ran Tao. Separations in proof complexity and TFNP. In 63rd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2022, Denver, CO, USA, October 31 - November 3, 2022, pages 1150-1161. IEEE, 2022. URL:
  21. Mika Göös, Pritish Kamath, Robert Robere, and Dmitry Sokolov. Adventures in monotone complexity and tfnp. Electron. Colloquium Comput. Complex., TR18-163, 2018. URL:
  22. 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:
  23. Mika Göös, Pritish Kamath, Katerina Sotiraki, and Manolis Zampetakis. On the complexity of modulo-q arguments and the chevalley-warning theorem. In Proceedings of the 35th Computational Complexity Conference, CCC '20, Dagstuhl, DEU, 2020. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL:
  24. Dima Grigoriev. Linear lower bound on degrees of positivstellensatz calculus proofs for the parity. Theor. Comput. Sci., 259(1-2):613-622, 2001. URL:
  25. Takashi Ishizuka. The complexity of the parity argument with potential. J. Comput. Syst. Sci., 120:14-41, 2021. URL:
  26. David S. Johnson, Christos H. Papadimitriou, and Mihalis Yannakakis. How easy is local search? J. Comput. Syst. Sci., 37(1):79-100, 1988. URL:
  27. Pritish Kamath. Some hardness escalation results in computational complexity theory. PhD thesis, Massachusetts Institute of Technology, 2019. Google Scholar
  28. Ruta Mehta. Constant rank two-player games are ppad-hard. SIAM J. Comput., 47(5):1858-1887, 2018. URL:
  29. Tsuyoshi Morioka. Classification of search problems and their definability in bounded arithmetic. Master’s thesis, University of Toronto, 2001. URL:
  30. Christos H. Papadimitriou. On the complexity of the parity argument and other inefficient proofs of existence. J. Comput. Syst. Sci., 48(3):498-532, 1994. URL:
  31. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log., 62(3):981-998, 1997. URL:
  32. Pavel Pudlák. On reducibility and symmetry of disjoint NP pairs. Theor. Comput. Sci., 295:323-339, 2003. URL:
  33. Pavel Pudlák. On the complexity of finding falsifying assignments for herbrand disjunctions. Arch. Math. Log., 54(7-8):769-783, 2015. URL:
  34. Alejandro A. Schäffer and Mihalis Yannakakis. Simple local search problems that are hard to solve. SIAM J. Comput., 20(1):56-87, 1991. URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail