An exponential lower bound for the bit pigeonhole principle in resolution over parities
Resolution over parities, $\mathrm{Res}(\oplus)$, is the characteristic-two version of resolution over linear equations: clauses are disjunctions of affine equations over $\mathbb F_2$. Superpolynomial size lower bounds were previously known only for restricted refutations: tree-like, regular, or of bounded depth. We p...