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.
@InProceedings{bhattacharya_et_al:LIPIcs.CCC.2024.23, author = {Bhattacharya, Sreejata Kishor and Chattopadhyay, Arkadev and Dvo\v{r}\'{a}k, Pavel}, title = {{Exponential Separation Between Powers of Regular and General Resolution over Parities}}, booktitle = {39th Computational Complexity Conference (CCC 2024)}, pages = {23:1--23:32}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-331-7}, ISSN = {1868-8969}, year = {2024}, volume = {300}, editor = {Santhanam, Rahul}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.23}, URN = {urn:nbn:de:0030-drops-204191}, doi = {10.4230/LIPIcs.CCC.2024.23}, annote = {Keywords: Proof Complexity, Regular Reslin, Branching Programs, Lifting} }
Feedback for Dagstuhl Publishing