TFNP Intersections Through the Lens of Feasible Disjunction

Authors Pavel Hubáček , Erfan Khaniki, Neil Thapen

Thumbnail PDF


  • Filesize: 0.89 MB
  • 24 pages

Document Identifiers

Author Details

Pavel Hubáček
  • Institute of Mathematics, Czech Academy of Sciences, Prague, Czech Republic
  • Charles University, Faculty of Mathematics and Physics, Prague, Czech Republic
Erfan Khaniki
  • Institute of Mathematics, Czech Academy of Sciences, Prague, Czech Republic
  • Charles University, Faculty of Mathematics and Physics, Prague, Czech Republic
Neil Thapen
  • Institute of Mathematics, Czech Academy of Sciences, Prague, Czech Republic


We would like to thank Lukáš Folwarczný, Tuomas Hakoniemi, Yuhao Li, William Pires, Pavel Pudlák and Robert Robere for helpful discussions related to this work.

Cite AsGet BibTex

Pavel Hubáček, Erfan Khaniki, and Neil Thapen. TFNP Intersections Through the Lens of Feasible Disjunction. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 63:1-63:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


The complexity class CLS was introduced by Daskalakis and Papadimitriou (SODA 2010) to capture the computational complexity of important TFNP problems solvable by local search over continuous domains and, thus, lying in both PLS and PPAD. It was later shown that, e.g., the problem of computing fixed points guaranteed by Banach’s fixed point theorem is CLS-complete by Daskalakis et al. (STOC 2018). Recently, Fearnley et al. (J. ACM 2023) disproved the plausible conjecture of Daskalakis and Papadimitriou that CLS is a proper subclass of PLS∩PPAD by proving that CLS = PLS∩PPAD. To study the possibility of other collapses in TFNP, we connect classes formed as the intersection of existing subclasses of TFNP with the phenomenon of feasible disjunction in propositional proof complexity; where a proof system has the feasible disjunction property if, whenever a disjunction F ∨ G has a small proof, and F and G have no variables in common, then either F or G has a small proof. Based on some known and some new results about feasible disjunction, we separate the classes formed by intersecting the classical subclasses PLS, PPA, PPAD, PPADS, PPP and CLS. We also give the first examples of proof systems which have the feasible interpolation property, but not the feasible disjunction property.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Problems, reductions and completeness
  • Theory of computation → Complexity classes
  • TFNP
  • feasible disjunction
  • proof complexity
  • TFNP intersection classes


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


  1. Albert Atserias, Massimo Lauria, and Jakob Nordström. Narrow proofs may be maximally long. ACM Trans. Comput. Log., 17(3):19, 2016. URL:
  2. 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:
  3. Eli Ben-Sasson. Size-space tradeoffs for resolution. SIAM Journal on Computing, 38(6):2511-2525, 2009. Google Scholar
  4. 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:
  5. Joshua Buresh-Oppenheim. On the TFNP complexity of factoring., 2006.
  6. Samuel R. Buss. Lower bounds on Nullstellensatz proofs via designs. In Proof complexity and feasible arithmetics, DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 59-71. American Mathematical Society, Providence, RI, USA, 1998. Google Scholar
  7. Samuel R. Buss, Russell Impagliazzo, Jan Krajíček, Pavel Pudlák, Alexander A. Razborov, and Jiri Sgall. Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Computational Complexity, 6:256-298, 1996. Google Scholar
  8. Samuel R. Buss, Leszek Aleksander Kołodziejczyk, and Neil Thapen. Fragments of approximate counting. The Journal of Symbolic Logic, 79(2):496-525, 2014. Google Scholar
  9. Samuel R. Buss and Jan Krajíček. An application of boolean complexity to separation problems in bounded arithmetic. Proceedings of the London Mathematical Society, 3(1):1-21, 1994. Google Scholar
  10. Samuel R. Buss and Grigori Mints. The complexity of the disjunction and existential properties in intuitionistic logic. Annals of Pure and Applied Logic, 99(1-3):93-104, 1999. Google Scholar
  11. Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo. Using the groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the twenty-eighth annual ACM symposium on Theory of computing, pages 174-183, 1996. Google Scholar
  12. Stefan Dantchev, Nicola Galesi, Abdul Ghani, and Barnaby Martin. Proof complexity and the binary encoding of combinatorial principles. arXiv preprint arXiv:2008.02138, 2020. Google Scholar
  13. Stefan Dantchev, Barnaby Martin, and Mark Rhodes. Tight rank lower bounds for the Sherali-Adams proof system. Theoretical Computer Science, 410(21-23):2054-2063, 2009. Google Scholar
  14. Constantinos Daskalakis and Christos H. Papadimitriou. Continuous local search. In Dana Randall, editor, Proceedings of the Twenty-Second Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2011, San Francisco, California, USA, January 23-25, 2011, pages 790-804. SIAM, 2011. URL:
  15. Constantinos Daskalakis, Christos Tzamos, and Manolis Zampetakis. A converse to Banach’s fixed point theorem and its CLS-completeness. 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 44-50. ACM, 2018. URL:
  16. 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:
  17. Susanna de Rezende, Aaron Potechin, and Kilian Risse. Clique is hard on average for unary Sherali-Adams. In 64th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2023, Santa Cruz, CA, USA, November 6-9, 2023, 2023. To appear. Google Scholar
  18. 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:
  19. Michal Garlík. Failure of feasible disjunction property for k-DNF resolution and NP-hardness of automating it. CoRR, abs/2003.10230, 2020. URL:
  20. M. Göös, P. Kamath, R. Robere, and D. Sokolov. Adventures in Monotone Complexity and TFNP. In Avrim Blum, editor, 10th Innovations in Theoretical Computer Science Conference (ITCS 2019), volume 124 of Leibniz International Proceedings in Informatics (LIPIcs), pages 38:1-38:19, Dagstuhl, Germany, 2018. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. URL:
  21. 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:
  22. 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:
  23. Mika Göös, Pritish Kamath, Katerina Sotiraki, and Manolis Zampetakis. On the complexity of modulo-q arguments and the Chevalley-Warning theorem. In 35th Computational Complexity Conference, CCC 2020, July 28-31, 2020, Saarbrücken, Germany (Virtual Conference), volume 169, pages 19:1-19:42, 2020. Google Scholar
  24. Tuomas Hakoniemi. Feasible Interpolation for Polynomial Calculus and Sums-Of-Squares. In 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), volume 168 of Leibniz International Proceedings in Informatics (LIPIcs), pages 63:1-63:14, 2020. Google Scholar
  25. Tuomas Hakoniemi. Size bounds for algebraic and semialgebraic proof systems. PhD thesis, Universitat Politècnica de Catalunya, 2022. Google Scholar
  26. Alexandros Hollender. The classes PPA-k: Existence from arguments modulo k. Theor. Comput. Sci., 885:15-29, 2021. URL:
  27. Takashi Ishizuka. The complexity of the parity argument with potential. J. Comput. Syst. Sci., 120:14-41, 2021. URL:
  28. Dmitry Itsykson, Vsevolod Oparin, Mikhail Slabodkin, and Dmitry Sokolov. Tight lower bounds on the resolution complexity of perfect matching principles. Fundamenta Informaticae, 145(3):229-242, 2016. Google Scholar
  29. Emil Jeřábek. Frege systems for extensible modal logics. Annals of Pure and Applied Logic, 142(1-3):366-379, 2006. Google Scholar
  30. Emil Jeřábek. Integer factoring and modular square roots. J. Comput. Syst. Sci., 82(2):380-394, 2016. URL:
  31. Alan Johnson. Reductions and propositional proofs for total NP search problems. PhD thesis, University of California, San Diego, 2011. Google Scholar
  32. David S. Johnson, Christos H. Papadimitriou, and Mihalis Yannakakis. How easy is local search? (extended abstract). In 26th Annual Symposium on Foundations of Computer Science, Portland, Oregon, USA, 21-23 October 1985, pages 39-42, 1985. Google Scholar
  33. Pritish Kamath. Some hardness escalation results in computational complexity theory. PhD thesis, Massachusetts Institute of Technology, 2019. Google Scholar
  34. Leszek Aleksander Kolodziejczyk, Phuong Nguyen, and Neil Thapen. The provably total NP search problems of weak second order bounded arithmetic. Ann. Pure Appl. Log., 162(6):419-446, 2011. URL:
  35. Leszek Aleksander Kolodziejczyk and Neil Thapen. Approximate counting and NP search problems. J. Math. Log., 22(3):2250012:1-2250012:31, 2022. URL:
  36. Jan Krajíček, Alan Skelley, and Neil Thapen. NP search problems in low fragments of bounded arithmetic. J. Symb. Log., 72(2):649-672, 2007. URL:
  37. J. Krajíček. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. The Journal of Symbolic Logic, 62(2):457-486, 1997. Google Scholar
  38. Jan Krajíček. Bounded arithmetic, propositional logic, and complexity theory, volume 60 of Encyclopedia of mathematics and its applications. Cambridge University Press, 1995. Google Scholar
  39. Yuhao Li, William Pires, and Robert Robere. Intersection classes in TFNP and proof complexity. In Venkatesan Guruswami, editor, 15th Innovations in Theoretical Computer Science Conference, ITCS 2024, January 30 - February 2, 2024, University of California, Berkeley, California, USA, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. To appear. Google Scholar
  40. Nimrod Megiddo and Christos H. Papadimitriou. On total functions, existence theorems and computational complexity. Theor. Comput. Sci., 81(2):317-324, 1991. URL:
  41. Tsuyoshi Morioka. Classification of search problems and their definability in bounded arithmetic. Electron. Colloquium Comput. Complex., TR01-082, 2001. URL:
  42. Tsuyoshi Morioka. The relative complexity of local search heuristics and the iteration principle. Electron. Colloquium Comput. Complex., TR03-051, 2003. URL:
  43. 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:
  44. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log., 62(3):981-998, 1997. URL:
  45. Pavel Pudlák. On the complexity of the propositional calculus. In S. Barry Cooper and John K. Truss, editors, Sets and Proofs, London Mathematical Society Lecture Note Series, pages 197-218. Cambridge University Press, 1999. Google Scholar
  46. Pavel Pudlák. On reducibility and symmetry of disjoint NP pairs. Theor. Comput. Sci., 295:323-339, 2003. URL:
  47. Søren Riis. Independence in Bounded Arithmetic. PhD thesis, Oxford University, 1993. Google Scholar
  48. Steven Rudich. Super-bits, demi-bits, and NP/qpoly-natural proofs. In José D. P. Rolim, editor, Randomization and Approximation Techniques in Computer Science, International Workshop, RANDOM'97, volume 1269 of Lecture Notes in Computer Science, pages 85-93. Springer, 1997. URL:
  49. 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
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