Weizmann Logo
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



TR24-022 | 6th February 2024 21:29

Exponential Separation Between Powers of Regular and General Resolution Over Parities



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 Raz and Tzamaret (2008). Very recently, Efremenko, Garlik and Itsykson (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 exists short proofs of their unsatisfiability in ordinary, non-regular resolution. This is the first super-polynomial separation between the power of general ResLin and and that of regular ResLin for any natural notion of regularity.

Our argument, while building upon the work of Efremenko et al, uses additional ideas from the literature on lifting theorems.

ISSN 1433-8092 | Imprint