Lower Bounds for Regular Resolution over Parities

The proof system resolution over parities (Res(⊕)) operates with disjunctions of linear equations (linear clauses) over GF(2); it extends the resolution proof system by incorporating linear algebra over GF(2). Over the years, several exponential lower bounds on the size of tree-like refutations have been established. However, proving a superpolynomial lower bound on the size of dag-like Res(⊕) refutations remains a highly challenging open question. We prove an exponential lower bound for regular Res(⊕). Regular Res(⊕) is a subsystem of dag-like Res(⊕) that naturally extends regular resolution. This is the first known superpolynomial lower bound for a fragment of dag-like Res(⊕) which is exponentially stronger than tree-like Res(⊕). In the regular regime, resolving linear clauses C₁ and C₂ on a linear form f is permitted only if, for both i∈ {1,2}, the linear form f does not lie within the linear span of all linear forms that were used in resolution rules during the derivation of C_i. Namely, we show that the size of any regular Res(⊕) refutation of the binary pigeonhole principle BPHP_nⁿ⁺¹ is at least 2^{Ω(∛n/logn)}. A corollary of our result is an exponential lower bound on the size of a strongly read-once linear branching program solving a search problem. This resolves an open question raised by Gryaznov, Pudlak, and Talebanfard (CCC 2022). As a byproduct of our technique, we prove that the size of any tree-like Res(⊕) refutation of the weak binary pigeonhole principle BPHP_n^m is at least 2^Ω(n) using Prover-Delayer games. We also give a direct proof of a width lower bound: we show that any dag-like Res(⊕) refutation of BPHP_n^m contains a linear clause C with Ω(n) linearly independent equations.