Por Pavel Dvořák (TIFR / Charles University).

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. Very recently, Efremenko, Garlík, and Itsykson [STOC'24] proved the first exponential lower bounds on the size of ResLin proofs that were additionally restricted to be bottom-regular. Extending their work, I'll 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.

This is joint work with Sreejata Kishor Bhattacharya and Arkadev Chattopadhyay.