Document Open Access Logo

Amortized Closure and Its Applications in Lifting for Resolution over Parities

Authors Klim Efremenko , Dmitry Itsykson

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CCC.2025.8.pdf
  • Filesize: 0.84 MB
  • 24 pages
HTML5 Logo HTML (experimental)
LIPIcs.CCC.2025.8.html

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • lifting
  • resolution over parities
  • closure of linear forms
  • lower bounds
  • width
  • depth
  • size vs depth tradeoff

Metrics

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

Abstract

The notion of closure of a set of linear forms, first introduced by Efremenko, Garlik, and Itsykson [Klim Efremenko et al., 2024], has proven instrumental in proving lower bounds on the sizes of regular and bounded-depth Res(⊕) refutations [Klim Efremenko et al., 2024; Yaroslav Alekseev and Dmitry Itsykson, 2025]. In this work, we present amortized closure, an enhancement that retains the properties of original closure [Klim Efremenko et al., 2024] but offers tighter control on its growth. Specifically, adding a new linear form increases the amortized closure by at most one. We explore two applications that highlight the power of this new concept.
Utilizing our newly defined amortized closure, we extend and provide a succinct and elegant proof of the recent lifting theorem by Chattopadhyay and Dvorak [Arkadev Chattopadhyay and Pavel Dvorak, 2025]. Namely we show that for an unsatisfiable CNF formula φ and a 1-stifling gadget g: {0,1}^𝓁 → {0,1}, if the lifted formula φ∘g has a tree-like Res(⊕) refutation of size 2^d and width w, then φ has a resolution refutation of depth d and width w. The original theorem by Chattopadhyay and Dvorak [Arkadev Chattopadhyay and Pavel Dvorak, 2025] applies only to the more restrictive class of strongly stifling gadgets. 
As a more significant application of amortized closure, we show improved lower bounds for bounded-depth Res(⊕), extending the depth beyond that of Alekseev and Itsykson [Yaroslav Alekseev and Dmitry Itsykson, 2025]. Our result establishes an exponential lower bound for depth-Ω(n log n) Res(⊕) refutations of lifted Tseitin formulas, a notable improvement over the existing depth-Ω(n log log n) Res(⊕) lower bound.

Cite As Get BibTex

Klim Efremenko and Dmitry Itsykson. Amortized Closure and Its Applications in Lifting for Resolution over Parities. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 8:1-8:24, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CCC.2025.8

Author Details

Klim Efremenko
  • Ben-Gurion University of the Negev, Beer-Sheva, Israel
Dmitry Itsykson
  • Ben-Gurion University of the Negev, Beer-Sheva, Israel
  • On leave from Steklov Institute of Mathematics at St. Petersburg, Russia

Funding

Supported by European Research Council Grant No. 949707.

Acknowledgements

The authors thank Yaroslav Alekseev and Alexander Knop for fruitful discussions.

References

  1. M. Ajtai. ∑₁¹-formulae on finite structures. Annals of Pure and Applied Logic, 24(1):1-48, 1983. URL: https://doi.org/10.1016/0168-0072(83)90038-6.
  2. Miklós Ajtai. The complexity of the pigeonhole principle. Combinatorica, 14(4):417-433, 1994. URL: https://doi.org/10.1007/BF01302964.
  3. Yaroslav Alekseev and Dmitry Itsykson. Lifting to bounded-depth and regular resolutions over parities via games. In Proceedings of the 57th Annual ACM Symposium on Theory of Computing (STOC '25), June 23-27, 2025, Prague, Czechia. ACM, 2025. The full version is available as ECCC technical report TR24-128, Revision 1. URL: https://doi.org/10.1145/3717823.3718150.
  4. 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.
  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. 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.
  7. 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.
  8. Sam Buss and Neil Thapen. A simple supercritical tradeoff between size and height in resolution. Electron. Colloquium Comput. Complex., TR24-001, 2024. URL: https://eccc.weizmann.ac.il/report/2024/001.
  9. 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.
  10. Arkadev Chattopadhyay and Pavel Dvorak. Super-critical trade-offs in resolution over parities via lifting. In Srikanth Srinivasan, editor, 40th Computational Complexity Conference CCC 2025, August 05–08, 2025, Toronto, Canada, volume 339 of LIPIcs, 2025. Available as ECCC technical report TR24-132. URL: https://eccc.weizmann.ac.il/report/2024/132/.
  11. 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.
  12. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, March 1979. URL: https://doi.org/10.2307/2273702.
  13. 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. Electron. Colloquium Comput. Complex., TR24-185, 2024. URL: https://eccc.weizmann.ac.il/report/2024/185.
  14. Klim Efremenko, Michal Garlík, and Dmitry Itsykson. Lower bounds for regular resolution over parities. In Bojan Mohar, Igor Shinkar, and Ryan O'Donnell, editors, Proceedings of the 56th Annual ACM Symposium on Theory of Computing, STOC 2024, Vancouver, BC, Canada, June 24-28, 2024, pages 640-651. ACM, 2024. The full version is available as ECCC technical report TR23-187. URL: https://doi.org/10.1145/3618260.3649652.
  15. Noah Fleming, Toniann Pitassi, and Robert Robere. Extremely deep proofs. In Mark Braverman, editor, 13th Innovations in Theoretical Computer Science Conference, ITCS 2022, January 31 - February 3, 2022, Berkeley, CA, USA, volume 215 of LIPIcs, pages 70:1-70:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.ITCS.2022.70.
  16. Merrick Furst, James B. Saxe, and Michael Sipser. Parity, circuits, and the polynomial-time hierarchy. 22nd Annual Symposium on Foundations of Computer Science (sfcs 1981), pages 260-270, 1981. URL: https://doi.org/10.1109/SFCS.1981.35.
  17. Mika Göös, Gilbert Maystre, Kilian Risse, and Dmitry Sokolov. Supercritical tradeoffs for monotone circuits. Electron. Colloquium Comput. Complex., TR24-186, 2024. URL: https://eccc.weizmann.ac.il/report/2024/186.
  18. Svyatoslav Gryaznov, Sergei Ovcharov, and Artur Riazanov. Resolution over linear equations: Combinatorial games for tree-like size and space. ACM Trans. Comput. Theory, July 2024. Just Accepted. URL: https://doi.org/10.1145/3675415.
  19. 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.
  20. Vladimir Podolskii and Alexander Shekhovtsov. Randomized lifting to semi-structured communication complexity via linear diversity. Electron. Colloquium Comput. Complex., TR24-199, 2024. URL: https://eccc.weizmann.ac.il/report/2024/199.
  21. 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
  22. 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.
  23. 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.
  24. D.J.A. Welsh. Generalized versions of Hall’s theorem. Journal of Combinatorial Theory, Series B, 10(2):95-101, 1971. URL: https://doi.org/10.1016/0095-8956(71)90069-4.
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