Document Open Access Logo

Super-Critical Trade-Offs in Resolution over Parities via Lifting

Authors Arkadev Chattopadhyay , Pavel Dvořák

PDF HTML 5

Files

Thumbnail PDF
PDF
LIPIcs.CCC.2025.24.pdf
  • Filesize: 0.82 MB
  • 19 pages
HTML5 Logo HTML (experimental)
LIPIcs.CCC.2025.24.html

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof complexity
  • Lifting
  • Resolution over parities

Metrics

Abstract

Razborov [Alexander A. Razborov, 2016] exhibited the following surprisingly strong trade-off phenomenon in propositional proof complexity: for a parameter k = k(n), there exists k-CNF formulas over n variables, having resolution refutations of O(k) width, but every tree-like refutation of width n^{1-ε}/k needs size exp(n^Ω(k)). We extend this result to tree-like Resolution over parities, commonly denoted by Res(⊕), with parameters essentially unchanged. 
To obtain our result, we extend the lifting theorem of Chattopadhyay, Mande, Sanyal and Sherif [Arkadev Chattopadhyay et al., 2023] to handle tree-like affine DAGs. We introduce additional ideas from linear algebra to handle forget nodes along long paths.

Cite As Get BibTex

Arkadev Chattopadhyay and Pavel Dvořák. Super-Critical Trade-Offs in Resolution over Parities via Lifting. In 40th Computational Complexity Conference (CCC 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 339, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CCC.2025.24

Author Details

Arkadev Chattopadhyay
  • Tata Institute of Fundamental Research, Mumbai, India
Pavel Dvořák
  • Charles University, Prague, Czech Republic

Funding

  • Chattopadhyay, Arkadev: Funded by the Department of Atomic Energy, Government of India, under project no. RTI4001, and a Google India Research Award.
  • Dvořák, Pavel: Major portion of work done as a visiting fellow at TIFR. Supported by Czech Science Foundation GAČR grant #22-14872O.

Acknowledgements

We would like to thank an anonymous reviewer for pointing out the short and elegant proof of Theorem 10 that we include here. Our original proof was complicated.

References

  1. Yaroslav Alekseev and Dmitry Itsykson. Lifting to regular resolution over parities via games. Electron. Colloquium Comput. Complex., TR24-128, 2024. URL: https://eccc.weizmann.ac.il/report/2024/128.
  2. Sepehr Assadi, Gillat Kol, and Zhijun Zhang. Rounds vs communication tradeoffs for maximal independent sets. In 63rd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2022, Denver, CO, USA, October 31 - November 3, 2022, pages 1193-1204. IEEE, 2022. URL: https://doi.org/10.1109/FOCS54457.2022.00115.
  3. Paul Beame, Christopher Beck, and Russell Impagliazzo. Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. In Howard J. Karloff and Toniann Pitassi, editors, Proceedings of the 44th Symposium on Theory of Computing Conference, STOC 2012, New York, NY, USA, May 19 - 22, 2012, pages 213-232. ACM, 2012. URL: https://doi.org/10.1145/2213977.2213999.
  4. 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, January 10-13, 2023, MIT, Cambridge, Massachusetts, USA, volume 251 of LIPIcs, pages 14:1-14:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.ITCS.2023.14.
  5. 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.
  6. Eli Ben-Sasson. Size space tradeoffs for resolution. In John H. Reif, editor, Proceedings on 34th Annual ACM Symposium on Theory of Computing, May 19-21, 2002, Montréal, Québec, Canada, pages 457-464. ACM, 2002. URL: https://doi.org/10.1145/509907.509975.
  7. Christoph Berkholz, Moritz Lichter, and Harry Vinall-Smeeth. Supercritical size-width tree-like resolution trade-offs for graph isomorphism, 2024. URL: https://doi.org/10.48550/arXiv.2407.17947.
  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, Arkadev Chattopadhyay, and Pavel Dvořák. Exponential Separation Between Powers of Regular and General Resolution over Parities. In Rahul Santhanam, editor, 39th Computational Complexity Conference (CCC 2024), volume 300 of Leibniz International Proceedings in Informatics (LIPIcs), pages 23:1-23:32, Dagstuhl, Germany, 2024. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CCC.2024.23.
  10. Mark Braverman and Rotem Oshman. A rounds vs. communication tradeoff for multi-party set disjointness. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 144-155. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/FOCS.2017.22.
  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. 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, 2024. URL: https://doi.org/10.48550/arXiv.2411.14267.
  13. 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. URL: https://doi.org/10.1145/3618260.3649652.
  14. 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.
  15. Lance Fortnow. Time-space tradeoffs for satisfiability. J. Comput. Syst. Sci., 60(2):337-353, 2000. URL: https://doi.org/10.1006/jcss.1999.1671.
  16. Lance Fortnow, Richard J. Lipton, Dieter van Melkebeek, and Anastasios Viglas. Time-space lower bounds for satisfiability. J. ACM, 52(6):835-865, 2005. URL: https://doi.org/10.1145/1101821.1101822.
  17. Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds from resolution. Theory Comput., 16:1-30, 2020. Preliminary version in STOC 2018. URL: https://doi.org/10.4086/TOC.2020.V016A013.
  18. Mika Göös, Gilbert Maystre, Kilian Risse, and Dmitry Sokolov. Supercritical tradeoffs for monotone circuits, 2024. URL: https://doi.org/10.48550/arXiv.2411.14268.
  19. 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.
  20. 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.
  21. Noam Nisan and Avi Wigderson. Rounds in communication complexity revisited. SIAM J. Comput., 22(1):211-219, 1993. URL: https://doi.org/10.1137/0222016.
  22. Pavel Pudlák. On extracting computations from propositional proofs (a survey). In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, volume 8 of LIPIcs, pages 30-41. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.30.
  23. Alexander A. Razborov. Unprovability of lower bounds on circuit size in certain fragments of bounded-arithmetic. Izvestiya. Math., 59(1):205-227, 1995. Google Scholar
  24. 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.
  25. Dmitry Sokolov. Dag-like communication and its applications. In Pascal Weil, editor, Computer Science - Theory and Applications - 12th International Computer Science Symposium in Russia, CSR 2017, Kazan, Russia, June 8-12, 2017, Proceedings, volume 10304 of Lecture Notes in Computer Science, pages 294-307. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-58747-9_26.
  26. R. Ryan Williams. Time-space tradeoffs for counting NP solutions modulo integers. Comput. Complex., 17(2):179-219, 2008. URL: https://doi.org/10.1007/s00037-008-0248-y.
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