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 1 and C 2 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 n +1 is at least 2 Ω(∛ 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 (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.

Authors

• Klim Efremenko
• Michal Garlík
• Dmitry Itsykson

Keywords

• binary pigeonhole principle
• lower bounds
• proof complexity
• regular resolution
• resolution over linear equations