ECCC-Report TR23-187https://eccc.weizmann.ac.il/report/2023/187Comments and Revisions published for TR23-187en-usTue, 28 Nov 2023 13:47:06 +0200
Paper TR23-187
| Lower bounds for regular resolution over parities |
Dmitry Itsykson,
Michal Garlik,
Klim Efremenko
https://eccc.weizmann.ac.il/report/2023/187The 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.Tue, 28 Nov 2023 13:47:06 +0200https://eccc.weizmann.ac.il/report/2023/187