The proof system resolution over parities (Res($\oplus$)) operates with disjunctions of linear equations (linear clauses) over $\mathbb{F}_2$; it extends the resolution proof system by incorporating linear algebra over $\mathbb{F}_2$. 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 $C_1$ and $C_2$ 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 $C_i$.

Namely, we show that the size of any regular $\resoplus$ refutation of the binary pigeonhole principle BPHP$^{n+1}_{n}$ is at least $2^{\Omega(\sqrt[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 (CCC 2022).

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.

A misspelling in Yan Zhong's last name was fixed.
Added a section with open questions and further research.

The proof system resolution over parities (Res($\oplus$)) operates with disjunctions of linear equations (linear clauses) over $\mathbb{F}_2$; it extends the resolution proof system by incorporating linear algebra over $\mathbb{F}_2$. 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 $C_1$ and $C_2$ 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 $C_i$.

Namely, we show that the size of any regular Res($\oplus$) refutation of the binary pigeonhole principle BPHP$^{n+1}_{n}$ is at least $2^{\Omega(\sqrt[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 (CCC 2022).

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.

Minor changes: some misprints were fixed, and several explanations were added.

The proof system resolution over parities (Res($\oplus$)) operates with disjunctions of linear equations (linear clauses) over $\mathbb{F}_2$; it extends the resolution proof system by incorporating linear algebra over $\mathbb{F}_2$. 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 $C_1$ and $C_2$ 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 $C_i$.

Namely, we show that the size of any regular $\resoplus$ refutation of the binary pigeonhole principle BPHP$^{n+1}_{n}$ is at least $2^{\Omega(\sqrt[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 (CCC 2022).

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.