קלים יפרמנקו

The proof system resolution over parities (Res(\oplus)) operates with disjunctions of linear equations (linear clauses) over \BbbF2; it extends the resolution proof system by incorporating linear algebra over \BbbF2. Over the years, several exponential lower bounds on the size of tree-like Res(\oplus) refutations have been established. However, proving a superpolynomial lower bound on the size of dag-like Res(\oplus) refutations remains a highly challenging open question. We prove an exponential lower bound for regular Res(\oplus). Regular Res(\oplus) is a subsystem of dag-like Res(\oplus) that naturally extends regular resolution. This is the first known superpolynomial lower bound for a fragment of dag-like Res(\oplus) which is exponentially stronger than tree-like Res(\oplus). In the regular regime, resolving linear clauses C1 and C2 on a linear form f is permitted only if, for both i \in \{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(\oplus) refutation of the binary pigeonhole principle BPHPⁿ_n⁺¹ is at least 2^{\Omega(\surd3 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, Pudl\'ak, and Talebanfard [Proceedings of the 37th Computational Complexity Conference, LIPIcs Leibniz Int. Proc. Inform. 234, S. Lovett, ed., Schloss Dagstuhl - Leibniz-Zentrum f\" ur Informatik, 2022, pp. 1-16]. As a byproduct of our technique, we prove that the size of any tree-like Res(\oplus) refutation of the weak binary pigeonhole principle BPHP^m_n is at least 2^\Omega(n⁾ using Prover-Delayer games. We also give a direct proof of a width lower bound: we show that any dag-like Res(\oplus) refutation of BPHP^m_n contains a linear clause C with \Omega(n) linearly independent equations.