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.
(1)We improve the lower bound in Lemma 15 to $n^{1/3}$ from $n^{1/6}$. This improvement propagates all the way to improve our main result, Theorem 1, by improving the lower bound to $M^{1/12}$ from $M^{1/24}$.
(2)There were typos in the statement of Theorem 5 that have now been fixed.
(3)A new paragraph has been added to Intro making more comparisons with some of the formulas considered in earlier work.
(4) Added more material to Section 3. In particular, we have a subsection discussing the model of strongly read-once linear branching programs considered in the work of Gryaznov et. al. and the model we consider here.
(5).Section 8 on future directions added.
Several other stylistic changes, fixing typos etc.
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.
