Document Open Access Logo

Exponential Separation Between Powers of Regular and General Resolution over Parities

Authors Sreejata Kishor Bhattacharya, Arkadev Chattopadhyay, Pavel Dvořák

PDF

File

Thumbnail PDF
PDF
LIPIcs.CCC.2024.23.pdf
  • Filesize: 0.87 MB
  • 32 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof Complexity
  • Regular Reslin
  • Branching Programs
  • Lifting

Metrics

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

Abstract

Proving super-polynomial lower bounds on the size of proofs of unsatisfiability of Boolean formulas using resolution over parities is an outstanding problem that has received a lot of attention after its introduction by Itsykson and Sokolov [Dmitry Itsykson and Dmitry Sokolov, 2014]. Very recently, Efremenko, Garlík and Itsykson [Klim Efremenko et al., 2023] proved the first exponential lower bounds on the size of ResLin proofs that were additionally restricted to be bottom-regular. We show that there are formulas for which such regular ResLin proofs of unsatisfiability continue to have exponential size even though there exist short proofs of their unsatisfiability in ordinary, non-regular resolution. This is the first super-polynomial separation between the power of general ResLin and that of regular ResLin for any natural notion of regularity. 
Our argument, while building upon the work of Efremenko et al. [Klim Efremenko et al., 2023], uses additional ideas from the literature on lifting theorems.

Cite As Get BibTex

Sreejata Kishor Bhattacharya, Arkadev Chattopadhyay, and Pavel Dvořák. Exponential Separation Between Powers of Regular and General Resolution over Parities. In 39th Computational Complexity Conference (CCC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 300, pp. 23:1-23:32, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CCC.2024.23

Author Details

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

Funding

  • Chattopadhyay, Arkadev: Partially funded by the Department of Atomic Energy and a Google India Research Award.
  • Dvořák, Pavel: Work done entirely at TIFR. Supported by Czech Science Foundation GAČR grant #22-14872O.

References

  1. Michael Alekhnovich, Jan Johannsen, Toniann Pitassi, and Alasdair Urquhart. An exponential separation between regular and general resolution. Theory of Computing, 3(5):81-102, 2007. Preliminary version in STOC, 2002. URL: https://doi.org/10.4086/toc.2007.v003a005.
  2. 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.
  3. Arkadev Chattopadhyay, Yuval Filmus, Sajin Koroth, Or Meir, and Toniann Pitassi. Query-to-communication lifting using low-discrepancy gadgets. SIAM J. Comput., 50(1):171-210, 2021. Preliminary version in ICALP, 2019. URL: https://doi.org/10.1137/19M1310153.
  4. 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.
  5. Eshan Chattopadhyay and Jyun-Jie Liao. Hardness against linear branching programs and more. Electron. Colloquium Comput. Complex., TR22-153, 2022. URL: https://arxiv.org/abs/TR22-153.
  6. Eshan Chattopadhyay and Jyun-Jie Liao. Hardness against linear branching programs and more. In Amnon Ta-Shma, editor, 38th Computational Complexity Conference, CCC 2023, July 17-20, 2023, Warwick, UK, volume 264 of LIPIcs, pages 9:1-9:27. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPIcs.CCC.2023.9.
  7. Klim Efremenko, Michal Garlík, and Dmitry Itsykson. Lower bounds for regular resolution over parities. Electron. Colloquium Comput. Complex., TR23-187, 2023. URL: https://arxiv.org/abs/TR23-187.
  8. 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.
  9. Mika Göös, Toniann Pitassi, and Thomas Watson. Query-to-communication lifting for BPP. SIAM J. Comput., 49(4), 2020. Preliminary version in FOCS 2017. URL: https://doi.org/10.1137/17M115339X.
  10. Svyatoslav Gryaznov, Pavel Pudlák, and Navid Talebanfard. Linear branching programs and directional affine extractors. In Shachar Lovett, editor, 37th Computational Complexity Conference, CCC 2022, July 20-23, 2022, Philadelphia, PA, USA, volume 234 of LIPIcs, pages 4:1-4:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.CCC.2022.4.
  11. 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.
  12. Dmitry Itsykson and Dmitry Sokolov. Resolution over linear equations modulo two. Annals of Pure and Applied Logic, 171(1):102722, 2020. URL: https://doi.org/10.1016/j.apal.2019.102722.
  13. Xin Li. Two source extractors for asymptotically optimal entropy, and (many) more. In 2023 IEEE 64th Annual Symposium on Foundations of Computer Science (FOCS), pages 1271-1281, 2023. URL: https://doi.org/10.1109/FOCS57990.2023.00075.
  14. Xin Li and Yan Zhong. Explicit directional affine extractors and improved hardness for linear branching programs. CoRR, abs/2304.11495, 2023. URL: https://doi.org/10.48550/arXiv.2304.11495.
  15. 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.
  16. Ran Raz and Iddo Tzameret. Resolution over linear equations and multilinear proofs. Ann. Pure Appl. Log., 155(3):194-224, 2008. URL: https://doi.org/10.1016/J.APAL.2008.04.001.
  17. 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
  18. 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.
  19. 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.
  20. Alasdair Urquhart. A near-optimal separation of regular and general resolution. SIAM J. Comput., 40(1):107-121, 2011. URL: https://doi.org/10.1137/090772897.
  21. Marc Vinyals, Jan Elffers, Jan Johannsen, and Jakob Nordström. Simplified and improved separations between regular and general resolution by lifting. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, Alghero, Italy, July 3-10, 2020, Proceedings, volume 12178 of Lecture Notes in Computer Science, pages 182-200. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_14.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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