Exponential Separation Between Powers of Regular and General Resolution Over Parities
CoRR(2024)
摘要
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ík 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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要