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 [Ann. Pure Appl. Log.'08]. Very recently, Efremenko, Garl\'ik and Itsykson [ECCC'23] 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.

翻译：证明布尔公式不可满足性在奇偶性解析（resolution over parities）下证明规模的超多项式下界是一个突出难题，自Raz和Tzamaret [Ann. Pure Appl. Log.'08]引入以来备受关注。近期，Efremenko、Garlík和Itsykson [ECCC'23]证明了在额外限制为底正则（bottom-regular）的ResLin证明规模上的首个指数下界。我们表明，存在一些公式，其正则ResLin不可满足性证明规模仍为指数级，尽管这些公式在普通非正则解析（non-regular resolution）中存在简短证明。这是针对任意自然正则性概念，首次在一般ResLin与正则ResLin能力之间建立超多项式分离。我们的论证在Efremenko等人工作的基础上，进一步借鉴了提升定理（lifting theorems）文献中的新思路。