Lifting to Bounded-Depth and Regular Resolutions over Parities via Games

Proving superpolynomial lower bounds on proof size in the proof system resolution over parities (Res(⊕)) remains a significant open challenge. A recent breakthrough by Efremenko, Garlik, and Itsykson (STOC 2024) established an exponential lower bound for regular Res(⊕). In this work, we introduce a lifting technique for regular Res(⊕), applicable to a wide range of formulas. Specifically, we develop a method that transforms any formula with large resolution depth into a formula requiring exponential-size regular Res(⊕) refutations. This transformation is achieved through a combination of mixing and constant-size lifting. Using this approach, we provide an alternative and improved separation between resolution and regular Res(⊕), originally proved by Bhattacharya, Chattopadhyay, and Dvorak (CCC 2024). We construct an n-variable formula with a polynomial-size resolution refutation of depth O(√n), yet requires regular Res(⊕) refutations of size 2Ω(√n). Furthermore, we apply our technique to establish an exponential lower bound on the size of depth-cnloglogn Res(⊕) refutations, where n is the number of variables in the refuted formula, and c is a constant. The hard instances in this setting are Tseitin formulas lifted with the Maj5 gadget. Since even depth-n Res(⊕) captures all possible definitions of regular Res(⊕), our result yields an exponential lower bound for top-regular Res(⊕), resolving an open question posed by Gryaznov, Pudlák, and Talebanfard (CCC 2022).