Document Open Access Logo

Supercritical Tradeoff Between Size and Depth for Resolution over Parities

Authors Dmitry Itsykson , Alexander Knop

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITCS.2026.81.pdf
  • Filesize: 0.78 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • lifting theorems
  • resolution depth
  • resolution over parities
  • resolution width
  • supercritical tradeoff

Metrics

Abstract

Alekseev and Itsykson (STOC 2025) proved the existence of an unsatisfiable CNF formula such that any resolution over parities (Res(⊕)) refutation must either have exponential size (in the formula size) or superlinear depth (in the number of variables). In this paper, we extend this result by constructing a formula with the same hardness properties, but which additionally admits a resolution refutation of quasi-polynomial size. This establishes a supercritical tradeoff between size and depth for resolution over parities.
The proof builds on the framework of Alekseev and Itsykson and relies on a lifting argument applied to the supercritical tradeoff between width and depth in resolution, proposed by Buss and Thapen (IPL 2026).

Cite As Get BibTex

Dmitry Itsykson and Alexander Knop. Supercritical Tradeoff Between Size and Depth for Resolution over Parities. In 17th Innovations in Theoretical Computer Science Conference (ITCS 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 362, pp. 81:1-81:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ITCS.2026.81

Author Details

Dmitry Itsykson
  • Ben-Gurion University of the Negev, Be'er-Sheva, Israel
  • On leave from Steklov Institute of Mathematics at St. Petersburg, Russia
Alexander Knop
  • Google Research, New York, NY, USA

Funding

  • Itsykson, Dmitry: Supported by European Research Council Grant No. 949707.

Acknowledgements

The authors thank Yaroslav Alekseev and Artur Riazanov for fruitful discussions.

References

  1. Miklós Ajtai. The complexity of the pigeonhole principle. Combinatorica, 14(4):417-433, 1994. URL: https://doi.org/10.1007/BF01302964.
  2. Yaroslav Alekseev and Dmitry Itsykson. Lifting to bounded-depth and regular resolutions over parities via games. In Michal Koucký and Nikhil Bansal, editors, Proceedings of the 57th Annual ACM Symposium on Theory of Computing, STOC 2025, Prague, Czechia, June 23-27, 2025, pages 584-595. ACM, 2025. URL: https://doi.org/10.1145/3717823.3718150.
  3. Albert Atserias and Víctor Dalmau. A combinatorial characterization of resolution width. Journal of Computer and System Sciences, 74(3):323-334, 2008. Computational Complexity 2003. URL: https://doi.org/10.1016/j.jcss.2007.06.025.
  4. 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.
  5. Paul Beame and Sajin Koroth. On Disperser/Lifting Properties of the Index and Inner-Product Functions. In Yael Tauman Kalai, editor, 14th Innovations in Theoretical Computer Science Conference (ITCS 2023), volume 251 of Leibniz International Proceedings in Informatics (LIPIcs), pages 14:1-14:17, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITCS.2023.14.
  6. Chris Beck, Jakob Nordström, and Bangsheng Tang. Some trade-off results for polynomial calculus: extended abstract. In Dan Boneh, Tim Roughgarden, and Joan Feigenbaum, editors, Symposium on Theory of Computing Conference, STOC'13, Palo Alto, CA, USA, June 1-4, 2013, pages 813-822. ACM, 2013. URL: https://doi.org/10.1145/2488608.2488711.
  7. Christoph Berkholz. On the complexity of finding narrow proofs. In 53rd Annual IEEE Symposium on Foundations of Computer Science, FOCS 2012, New Brunswick, NJ, USA, October 20-23, 2012, pages 351-360. IEEE Computer Society, 2012. URL: https://doi.org/10.1109/FOCS.2012.48.
  8. Christoph Berkholz and Jakob Nordström. Supercritical space-width trade-offs for resolution. SIAM J. Comput., 49(1):98-118, 2020. URL: https://doi.org/10.1137/16M1109072.
  9. Sreejata Kishor Bhattacharya and Arkadev Chattopadhyay. Exponential lower bounds on the size of reslin proofs of nearly quadratic depth. Electron. Colloquium Comput. Complex., TR25-106, 2025. URL: https://eccc.weizmann.ac.il/report/2025/106.
  10. Sreejata Kishor Bhattacharya, Arkadev Chattopadhyay, and Pavel Dvorák. Exponential separation between powers of regular and general resolution over parities. In Rahul Santhanam, editor, 39th Computational Complexity Conference, CCC 2024, July 22-25, 2024, Ann Arbor, MI, USA, volume 300 of LIPIcs, pages 23:1-23:32. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CCC.2024.23.
  11. Sam Buss and Neil Thapen. A simple supercritical tradeoff between size and height in resolution. Information Processing Letters, 191:106589, 2026. The preprint is available at https://eccc.weizmann.ac.il/report/2024/001. URL: https://doi.org/10.1016/j.ipl.2025.106589.
  12. Farzan Byramji and Russell Impagliazzo. Lifting to randomized parity decision trees. Electron. Colloquium Comput. Complex., TR24-202, 2024. URL: https://eccc.weizmann.ac.il/report/2024/202.
  13. Farzan Byramji and Russell Impagliazzo. Lower bounds for the bit pigeonhole principle in bounded-depth resolution over parities. Electron. Colloquium Comput. Complex., TR25-118, 2025. URL: https://eccc.weizmann.ac.il/report/2025/118.
  14. Arkadev Chattopadhyay and Pavel Dvorák. Super-critical trade-offs in resolution over parities via lifting. In Srikanth Srinivasan, editor, 40th Computational Complexity Conference, CCC 2025, August 5-8, 2025, Toronto, Canada, volume 339 of LIPIcs, pages 24:1-24:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CCC.2025.24.
  15. Arkadev Chattopadhyay, Nikhil S. Mande, Swagato Sanyal, and Suhail Sherif. Lifting to parity decision trees via stifling. 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 33:1-33:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.ITCS.2023.33.
  16. Susanna F. de Rezende, Noah Fleming, Duri Andrea Janett, Jakob Nordström, and Shuo Pang. Truly supercritical trade-offs for resolution, cutting planes, monotone circuits, and weisfeiler–leman. In Proceedings of the 57th Annual ACM Symposium on Theory of Computing, STOC '25, pages 1371-1382, New York, NY, USA, 2025. Association for Computing Machinery. URL: https://doi.org/10.1145/3717823.3718271.
  17. Klim Efremenko, Michal Garlík, and Dmitry Itsykson. Lower bounds for regular resolution over parities. SIAM J. Comput., 54(4):887-915, 2025. Preliminary version appeared in Proceedings of STOC 2024. URL: https://doi.org/10.1137/24M1696640.
  18. Klim Efremenko and Dmitry Itsykson. Amortized closure and its applications in lifting for resolution over parities. In Srikanth Srinivasan, editor, 40th Computational Complexity Conference, CCC 2025, August 5-8, 2025, Toronto, Canada, volume 339 of LIPIcs, pages 8:1-8:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CCC.2025.8.
  19. Noah Fleming, Toniann Pitassi, and Robert Robere. Extremely Deep Proofs. In Mark Braverman, editor, 13th Innovations in Theoretical Computer Science Conference (ITCS 2022), volume 215 of Leibniz International Proceedings in Informatics (LIPIcs), pages 70:1-70:23, Dagstuhl, Germany, 2022. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ITCS.2022.70.
  20. Michal Garlík and Leszek Aleksander Kolodziejczyk. Some subsystems of constant-depth frege with parity. ACM Trans. Comput. Log., 19(4):29:1-29:34, 2018. URL: https://doi.org/10.1145/3243126.
  21. Mika Göös, Gilbert Maystre, Kilian Risse, and Dmitry Sokolov. Supercritical tradeoffs for monotone circuits. In Michal Koucký and Nikhil Bansal, editors, Proceedings of the 57th Annual ACM Symposium on Theory of Computing, STOC 2025, Prague, Czechia, June 23-27, 2025, pages 1359-1370. ACM, 2025. URL: https://doi.org/10.1145/3717823.3718229.
  22. Svyatoslav Gryaznov, Sergei Ovcharov, and Artur Riazanov. Resolution over linear equations: Combinatorial games for tree-like size and space. ACM Trans. Comput. Theory, 16(3):15:1-15:15, 2024. URL: https://doi.org/10.1145/3675415.
  23. Dmitry Itsykson and Artur Riazanov. Proof complexity of natural formulas via communication arguments. In Valentine Kabanets, editor, 36th Computational Complexity Conference, CCC 2021, July 20-23, 2021, Toronto, Ontario, Canada (Virtual Conference), volume 200 of LIPIcs, pages 3:1-3:34. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CCC.2021.3.
  24. Dmitry Itsykson and Dmitry Sokolov. Lower bounds for splittings by linear combinations. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part II, volume 8635 of Lecture Notes in Computer Science, pages 372-383. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44465-8_32.
  25. Dmitry Itsykson and Dmitry Sokolov. Resolution over linear equations modulo two. Ann. Pure Appl. Log., 171(1), 2020. URL: https://doi.org/10.1016/J.APAL.2019.102722.
  26. Jan Krajíček. 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.
  27. Pavel Pudlák and Russell Impagliazzo. A lower bound for DLL algorithms for k-sat (preliminary version). In David B. Shmoys, editor, Proceedings of the Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, January 9-11, 2000, San Francisco, CA, USA, pages 128-136. ACM/SIAM, 2000. URL: http://dl.acm.org/citation.cfm?id=338219.338244.
  28. A. A. Razborov. Lower bounds on the size of bounded depth circuits over a complete basis with logical addition. Mat. Zametki, 41:598-607, 1987. Google Scholar
  29. Alexander A. Razborov. A new kind of tradeoffs in propositional proof complexity. J. ACM, 63(2):16:1-16:14, 2016. URL: https://doi.org/10.1145/2858790.
  30. Alexander A. Razborov. On the width of semialgebraic proofs and algorithms. Math. Oper. Res., 42(4):1106-1134, 2017. URL: https://doi.org/10.1287/MOOR.2016.0840.
  31. Alexander A. Razborov. On space and depth in resolution. Comput. Complex., 27(3):511-559, 2018. URL: https://doi.org/10.1007/S00037-017-0163-1.
  32. Roman Smolensky. Algebraic methods in the theory of lower bounds for boolean circuit complexity. In Alfred V. Aho, editor, Proceedings of the 19th Annual ACM Symposium on Theory of Computing, 1987, New York, New York, USA, pages 77-82. ACM, 1987. URL: https://doi.org/10.1145/28395.28404.
  33. Alasdair Urquhart. Hard examples for resolution. Journal of the ACM, 34(1):209-219, 1987. URL: https://doi.org/10.1145/7531.8928.
  34. Alasdair Urquhart. The depth of resolution proofs. Stud Logica, 99(1-3):349-364, 2011. URL: https://doi.org/10.1007/S11225-011-9356-9.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact