Lower Bounds for Regular Resolution over Parities

The proof system resolution over parities (Res(⊕)) operates with disjunctions of linear equations (linear clauses) over F2; it extends the resolution proof system by incorporating linear algebra over F2. Over the years, several exponential lower bounds on the size of tree-like Res(⊕) 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 C1 and C2 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 Ci.

Namely, we show that the size of any regular Res(⊕) refutation of the binary pigeonhole principle BPHP n+1 n is at least 2 Ω( 3 √ n/ log n) . 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 [24].

As a byproduct of our technique, we prove that the size of any tree-like Res(⊕) refutation of the weak binary pigeonhole principle BPHP m n 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 m n contains a linear clause C with Ω(n) linearly independent equations.