Document Open Access Logo

Efficient Adversaries

Authors Erfan Khaniki , Ján Pich , Dmitry Sokolov

PDF

File

Thumbnail PDF
PDF
LIPIcs.CCC.2026.8.pdf
  • Filesize: 0.98 MB
  • 32 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Circuit complexity
  • Theory of computation → Complexity theory and logic
Keywords
  • proof complexity
  • circuit complexity
  • lower bounds
  • barriers
  • truth-table formula
  • pigeonhole principle

Metrics

Abstract

The size of Frege proofs can be characterized in terms of prover-adversary games of Pudlák and Buss. We consider a generalization of prover-adversary games to many standard proof systems and show that some of the major proof complexity lower bounds such as the constant-depth Frege lower bound for the pigeonhole principle based on the method of k-evaluations, the Resolution lower bound for the weak pigeonhole principle based on the method of pseudo-width and Razborov’s Res(k) lower bound for Nisan-Wigderson generators based on expansion and a width lower bound (which is used to derive the Res(k)-hardness of formulas expressing circuit lower bounds) are constructive in the sense that they yield efficient algorithms computing winning strategies of adversaries in the generalized games. This is in contrast with our second result saying that if (a) such a constructive lower bound exists for Extended Frege system EF for formulas expressing succinct circuit lower bounds for SAT and (b) EF is strong enough to prove efficiently the correctness of anticheckers for SAT, then it is easy to separate the canonical pair of EF.

Cite As Get BibTex

Erfan Khaniki, Ján Pich, and Dmitry Sokolov. Efficient Adversaries. In 41st Computational Complexity Conference (CCC 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 383, pp. 8:1-8:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CCC.2026.8

Author Details

Erfan Khaniki
  • University of Oxford, UK
Ján Pich
  • University of Oxford, UK
Dmitry Sokolov
  • Université de Montréal, Canada

Funding

  • Khaniki, Erfan: This work was supported by the Royal Society University Research Fellowship URF\R1\211106 "Proof complexity and circuit complexity: a unified approach".
  • Pich, Ján: This work was supported by the Royal Society University Research Fellowship URF\R1\211106 "Proof complexity and circuit complexity: a unified approach".
  • Sokolov, Dmitry: This work was supported by the Swiss State Secretariat for Education, Research, and Innovation (SERI) under contract number MB22.00026.

Acknowledgements

We are indebted to Moritz Müller for a simplification of the proof of Theorem 1, which allowed us to derive Theorem 2 for EF instead of G₁^*, and for many comments that clarified the presentation of the paper. We thank Neil Thapen for a correction of Lemma 19, Noel Arteche for pointing out to us that Item 2 in Theorem 1 implies NP ̸ ⊆ Circuit[n^{𝓁}], and Pavel Pudlák, Jan Krajíček and anonymous reviewers for suggestions and comments. This project was initiated at the Institute of Mathematics of the Czech Academy of Sciences. For the purpose of Open Access, the authors have applied a CC BY public copyright licence to any Author Accepted Manuscript version arising from this submission.

References

  1. Miklós Ajtai. The Complexity of the Pigeonhole Principle. Comb., 14(4):417-433, 1994. URL: https://doi.org/10.1007/BF01302964.
  2. Noel Arteche, Albert Atserias, Susanna F. de Rezende, and Erfan Khaniki. The Proof Analysis Problem. In 66th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2025, Sydney, Australia, December 14-17, 2025, pages 2555-2576, 2025. URL: https://doi.org/10.1109/FOCS63196.2025.00133.
  3. Noel Arteche, Erfan Khaniki, Ján Pich, and Rahul Santhanam. From Proof Complexity to Circuit Complexity via Interactive Protocols. In 51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, Tallinn, Estonia, July 8-12, 2024, pages 12:1-12:20, 2024. URL: https://doi.org/10.4230/LIPIcs.ICALP.2024.12.
  4. Albert Atserias and Moritz Müller. Automating Resolution is NP-Hard. J. ACM, 67(5):31:1-31:17, 2020. URL: https://doi.org/10.1145/3409472.
  5. Per Austrin and Kilian Risse. Sum-Of-Squares Lower Bounds for the Minimum Circuit Size Problem. In 38th Computational Complexity Conference, CCC 2023, Warwick, UK, July 17-20, 2023, pages 31:1-31:21, 2023. URL: https://doi.org/10.4230/LIPIcs.CCC.2023.31.
  6. Paul Beame and Toniann Pitassi. Propositional proof complexity: Past, present, and future. In Current Trends in Theoretical Computer Science, Entering the 21th Century, pages 42-70. World Scientific, 2001. Google Scholar
  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. Maria Luisa Bonet, Carlos Domingo, Ricard Gavaldà, Alexis Maciel, and Toniann Pitassi. Non-Automatizability of Bounded-Depth Frege Proofs. Comput. Complex., 13(1-2):47-68, 2004. URL: https://doi.org/10.1007/S00037-004-0183-5.
  9. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. On Interpolation and Automatization for Frege Systems. SIAM J. Comput., 29(6):1939-1967, 2000. URL: https://doi.org/10.1137/S0097539798353230.
  10. Samuel R. Buss. Bounded arithmetic. Princeton University, 1985. Google Scholar
  11. Samuel R. Buss. On model theory for intuitionistic bounded arithmetic with applications to independence results. In Feasible Mathematics: A Mathematical Sciences Institute Workshop, Ithaca, New York, June 1989, pages 27-47, 1990. Google Scholar
  12. Marco L. Carmosino, Russell Impagliazzo, Valentine Kabanets, and Antonina Kolokolova. Learning Algorithms from Natural Proofs. In 31st Conference on Computational Complexity, CCC 2016, Tokyo, Japan, May 29 - June 1, 2016, pages 10:1-10:24, 2016. URL: https://doi.org/10.4230/LIPIcs.CCC.2016.10.
  13. Lijie Chen, Shuichi Hirahara, Igor Carboni Oliveira, Ján Pich, Ninad Rajgopal, and Rahul Santhanam. Beyond Natural Proofs: Hardness Magnification and Locality. J. ACM, 69(4):25:1-25:49, 2022. URL: https://doi.org/10.1145/3538391.
  14. Lijie Chen, Jiatu Li, and Igor C. Oliveira. Reverse Mathematics of Complexity Lower Bounds. In 65th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2024, Chicago, IL, USA, October 27-30, 2024, pages 505-527, 2024. URL: https://doi.org/10.1109/FOCS61266.2024.00040.
  15. Lijie Chen, Ron D. Rothblum, and Roei Tell. Fiat-Shamir in the Plain Model from Derandomization (Or: Do Efficient Algorithms Believe that NP = PSPACE?). In Proceedings of the 57th Annual ACM Symposium on Theory of Computing, STOC 2025, Prague, Czechia, June 23-27, 2025, pages 977-985, 2025. URL: https://doi.org/10.1145/3717823.3718177.
  16. Stephen A. Cook. Feasibly Constructive Proofs and the Propositional Calculus. In Proceedings of the 7th Annual ACM Symposium on Theory of Computing, May 5-7, 1975, Albuquerque, New Mexico, USA, pages 83-97, 1975. Google Scholar
  17. Stephen A. Cook and Jan Krajícek. Consequences of the provability of NP ⊆ P/poly. J. Symb. Log., 72(4):1353-1371, 2007. URL: https://doi.org/10.2178/JSL/1203350791.
  18. Stephen A. Cook and Alasdair Urquhart. Functional Interpretations of Feasibly Constructive Arithmetic. Ann. Pure Appl. Log., 63(2):103-200, 1993. URL: https://doi.org/10.1016/0168-0072(93)90044-E.
  19. Ben Davis and Robert Robere. Res(log) Proves Bounded-Depth Frege Lower Bounds. ECCC, TR26-055, 2026. Google Scholar
  20. Susanna F. de Rezende, Jakob Nordström, Kilian Risse, and Dmitry Sokolov. Exponential Resolution Lower Bounds for Weak Pigeonhole Principle and Perfect Matching Formulas over Sparse Graphs. TheoretiCS, 4, 2025. URL: https://doi.org/10.46298/THEORETICS.25.9.
  21. Mika Göös. Communication Lower Bounds via Query Complexity. University of Toronto (Canada), 2016. Google Scholar
  22. Joshua A. Grochow and Toniann Pitassi. Circuit Complexity, Proof Complexity, and Polynomial Identity Testing: The Ideal Proof System. J. ACM, 65(6):37:1-37:59, 2018. URL: https://doi.org/10.1145/3230742.
  23. Svyatoslav Gryaznov and Navid Talebanfard. Bounded Depth Frege Lower Bounds for Random 3-CNFs via Deterministic Restrictions. arXiv, 2024. URL: https://doi.org/10.48550/arXiv.2403.02275.
  24. Shuichi Hirahara, Rahul Ilango, and Ryan Williams. Beating Brute Force for Compression Problems. In Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 659-670, 2024. URL: https://doi.org/10.1145/3618260.3649778.
  25. Emil Jerábek. Dual weak pigeonhole principle, Boolean complexity, and derandomization. Ann. Pure Appl. Log., 129(1-3):1-37, 2004. URL: https://doi.org/10.1016/J.APAL.2003.12.003.
  26. Ondřej Ježil and Dimitrios Tsintsilidas. Parallelism and Adaptivity in Student-Teacher Witnessing. arXiv, 2026. URL: https://arxiv.org/abs/2602.19934.
  27. Erfan Khaniki. Nisan-Wigderson Generators in Proof Complexity: New Lower Bounds. In 37th Computational Complexity Conference, CCC 2022, Philadelphia, PA, USA, July 20-23, 2022, pages 17:1-17:15, 2022. URL: https://doi.org/10.4230/LIPIcs.CCC.2022.17.
  28. Erfan Khaniki. Jump Operators, Interactive Proofs and Proof Complexity Generators. In 65th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2024, Chicago, IL, USA, October 27-30, 2024, pages 573-593, 2024. URL: https://doi.org/10.1109/FOCS61266.2024.00044.
  29. Jan Krajicek. Bounded arithmetic, propositional logic and complexity theory, volume 60. Cambridge University Press, 1995. Google Scholar
  30. Jan Krajíček. On the weak pigeonhole principle. Fundamenta Mathematicae, 170:123-140, 2001. Google Scholar
  31. Jan Krajícek. Implicit proofs. J. Symb. Log., 69(2):387-397, 2004. URL: https://doi.org/10.2178/JSL/1082418532.
  32. Jan Krajícek. On the Proof Complexity of the Nisan-Wigderson Generator based on a Hard NP ∩ coNP function. J. Math. Log., 11(1), 2011. URL: https://doi.org/10.1142/S0219061311000979.
  33. Jan Krajíček. On the computational complexity of finding hard tautologies. Bulletin of the London Mathematical Society, 46(1):111-125, 2014. Google Scholar
  34. Jan Krajíček. Proof complexity, volume 170. Cambridge University Press, 2019. Google Scholar
  35. Jan Krajíček. Proof Complexity Generators. Cambridge University Press, 2025. Google Scholar
  36. Jan Krajíček and Pavel Pudlák. Propositional provability and models of weak arithmetic. In International Workshop on Computer Science Logic, pages 193-210, 1989. Google Scholar
  37. Jan Krajícek and Pavel Pudlák. Some Consequences of Cryptographical Conjectures for S¹₂ and EF. Inf. Comput., 140(1):82-94, 1998. Google Scholar
  38. Jan Krajíček, Pavel Pudlák, and Alan Woods. An exponential lower bound to the size of bounded depth Frege proofs of the pigeonhole principle. Random structures & algorithms, 7(1):15-39, 1995. URL: https://doi.org/10.1002/RSA.3240070103.
  39. Jiatu Li and Igor C. Oliveira. Unprovability of Strong Complexity Lower Bounds in Bounded Arithmetic. In Proceedings of the 55th Annual ACM Symposium on Theory of Computing, STOC 2023, Orlando, FL, USA, June 20-23, 2023, pages 1051-1057, 2023. URL: https://doi.org/10.1145/3564246.3585144.
  40. Jiawei Li, Yuhao Li, and Hanlin Ren. Finding Bugs in Short Proofs: The Metamathematics of Resolution Lower Bounds . arXiv, 2026. URL: https://arxiv.org/abs/2411.15515.
  41. Richard J. Lipton and Neal E. Young. Simple strategies for large zero-sum games with applications to complexity theory. In Proceedings of the Twenty-Sixth Annual ACM Symposium on Theory of Computing, 23-25 May 1994, Montréal, Québec, Canada, pages 734-740, 1994. URL: https://doi.org/10.1145/195058.195447.
  42. Jiaqi Lu, Rahul Santhanam, and Iddo Tzameret. AC⁰[p]-Frege Cannot Efficiently Prove That Constant-Depth Algebraic Circuit Lower Bounds Are Hard. In 17th Innovations in Theoretical Computer Science Conference, ITCS 2026, Bocconi University, Milan, Italy, January 27-30, 2026, pages 99:1-99:25, 2026. Google Scholar
  43. Noam Mazor and Rafael Pass. The Non-Uniform Perebor Conjecture for Time-Bounded Kolmogorov Complexity Is False. In 15th Innovations in Theoretical Computer Science Conference, ITCS 2024, Berkeley, CA, USA, January 30 - February 2, 2024, pages 80:1-80:20, 2024. URL: https://doi.org/10.4230/LIPIcs.ITCS.2024.80.
  44. Moritz Müller and Ján Pich. Feasibly constructive proofs of succinct weak circuit lower bounds. Ann. Pure Appl. Log., 171(2), 2020. URL: https://doi.org/10.1016/J.APAL.2019.102735.
  45. Igor C. Oliveira. SIGACT News Complexity Theory Column 124 Meta-Mathematics of Computational Complexity Theory. SIGACT News, 56(1):41-68, 2025. URL: https://doi.org/10.1145/3726856.3726862.
  46. Ján Pich. Circuit lower bounds in bounded arithmetics. Ann. Pure Appl. Log., 166(1):29-45, 2015. URL: https://doi.org/10.1016/J.APAL.2014.08.004.
  47. Ján Pich. Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic. Log. Methods Comput. Sci., 11(2), 2015. URL: https://doi.org/10.2168/LMCS-11(2:8)2015.
  48. Ján Pich and Rahul Santhanam. Why are Proof Complexity Lower Bounds Hard? In 60th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2019, Baltimore, Maryland, USA, November 9-12, 2019, pages 1305-1324, 2019. URL: https://doi.org/10.1109/FOCS.2019.00080.
  49. Ján Pich and Rahul Santhanam. Strong co-nondeterministic lower bounds for NP cannot be proved feasibly. In STOC '21: 53rd Annual ACM SIGACT Symposium on Theory of Computing, Virtual Event, Italy, June 21-25, 2021, pages 223-233, 2021. URL: https://doi.org/10.1145/3406325.3451117.
  50. Jan Pich and Rahul Santhanam. Towards P≠ NP from Extended Frege lower bounds. J. ACM, 73(2), 2026. Google Scholar
  51. Toniann Pitassi, Paul Beame, and Russell Impagliazzo. Exponential Lower Bounds for the Pigeonhole Principle. Comput. Complex., 3:97-140, 1993. URL: https://doi.org/10.1007/BF01200117.
  52. 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.
  53. Pavel Pudlák and Samuel R. Buss. How to Lie Without Being (Easily) Convicted and the Length of Proofs in Propositional Calculus. In Computer Science Logic, 8th International Workshop, CSL '94, Kazimierz, Poland, September 25-30, 1994, Selected Papers, pages 151-162, 1994. URL: https://doi.org/10.1007/BFB0022253.
  54. Ran Raz. Resolution lower bounds for the weak pigeonhole principle. J. ACM, 51(2):115-138, 2004. URL: https://doi.org/10.1145/972639.972640.
  55. Alexander Razborov. Lower bounds on the monotone complexity of some Boolean function. In Soviet Math. Dokl., volume 31, pages 354-357, 1985. Google Scholar
  56. Alexander Razborov. Lower bounds on the size of bounded depth circuits over a complete basis with logical addition. Mathematical Notes of the Academy of Sciences of the USSR, 41(4):333-338, 1987. Google Scholar
  57. Alexander Razborov. On the Method of Approximations. In Proceedings of the 21st Annual ACM Symposium on Theory of Computing, May 14-17, 1989, Seattle, Washington, USA, pages 167-176, 1989. URL: https://doi.org/10.1145/73007.73023.
  58. Alexander Razborov. On provably disjoint NP-pairs. Aarhus Universitet. Basic Research in Computer Science [BRICS], 1994. Google Scholar
  59. Alexander Razborov. Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic. Izvestiya: mathematics, 59(1):205-227, 1995. Google Scholar
  60. Alexander Razborov. Lower Bounds for the Polynomial Calculus. Comput. Complex., 7(4):291-324, 1998. URL: https://doi.org/10.1007/S000370050013.
  61. Alexander Razborov. Improved Resolution Lower Bounds for the Weak Pigeonhole Principle. ECCC, TR01-055, 2001. URL: https://eccc.weizmann.ac.il/eccc-reports/2001/TR01-055/index.html.
  62. Alexander Razborov. Resolution lower bounds for the weak functional pigeonhole principle. Theor. Comput. Sci., 303(1):233-243, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00453-X.
  63. Alexander Razborov. Resolution lower bounds for perfect matching principles. J. Comput. Syst. Sci., 69(1):3-27, 2004. URL: https://doi.org/10.1016/J.JCSS.2004.01.004.
  64. Alexander Razborov. Pseudorandom generators hard for k-DNF resolution and polynomial calculus resolution. Annals of Mathematics, pages 415-472, 2015. Google Scholar
  65. Alexander Razborov and Steven Rudich. Natural Proofs. J. Comput. Syst. Sci., 55(1):24-35, 1997. URL: https://doi.org/10.1006/JCSS.1997.1494.
  66. Robert Robere. Unified lower bounds for monotone computation. University of Toronto (Canada), 2018. Google Scholar
  67. Rahul Santhanam and Iddo Tzameret. Iterated Lower Bound Formulas: A Diagonalization-Based Approach to Proof Complexity. SIAM Journal on Computing, pages STOC21-313, 2025. Google Scholar
  68. 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.
  69. Roman Smolensky. Algebraic Methods in the Theory of Lower Bounds for Boolean Circuit Complexity. In Proceedings of the 19th Annual ACM Symposium on Theory of Computing, 1987, New York, New York, USA, pages 77-82, 1987. URL: https://doi.org/10.1145/28395.28404.
  70. Ryan Williams. Strong ETH Breaks With Merlin and Arthur: Short Non-Interactive Proofs of Batch Evaluation. In 31st Conference on Computational Complexity, CCC 2016, Tokyo, Japan, May 29 - June 1, 2016, pages 2:1-2:17, 2016. URL: https://doi.org/10.4230/LIPIcs.CCC.2016.2.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact