2026-07-28T21:27:32Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:20419 2024-07-15T12:26:46Z ddc:004 open_access

Exponential Separation Between Powers of Regular and General Resolution over Parities Bhattacharya, Sreejata Kishor Chattopadhyay, Arkadev Dvořák, Pavel Proof Complexity Regular Reslin Branching Programs Lifting 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Sreejata Kishor Bhattacharya and Arkadev Chattopadhyay and Pavel Dvořák 2024 Is Part Of LIPIcs, Volume 300, 39th Computational Complexity Conference (CCC 2024) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CCC.2024.23 urn:nbn:de:0030-drops-204191 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CCC.2024.23 eng https://creativecommons.org/licenses/by/4.0/legalcode