ECCC-Report TR24-132https://eccc.weizmann.ac.il/report/2024/132Comments and Revisions published for TR24-132en-usFri, 06 Sep 2024 21:57:56 +0300
Paper TR24-132
| Super-critical Trade-offs in Resolution over Parities Via Lifting |
Arkadev Chattopadhyay,
Pavel Dvorak
https://eccc.weizmann.ac.il/report/2024/132Razborov [J. ACM, 2016] exhibited the following surprisingly strong trade-off phenomenon in propositional proof complexity: for a parameter $k = k(n)$, there exists $k$-CNF formulas over $n$ variables, having resolution refutations of $O(k)$ width, but every tree-like refutation of width $n^{1-\epsilon}/k$ needs size $\text{exp}\big(n^{\Omega(k)}\big)$. We extend this result to tree-like Resolution over parities, commonly denoted by $\text{Res}(\oplus)$, with parameters essentially unchanged.
To obtain our result, we extend the lifting theorem of Chattopadhyay, Mande, Sanyal and Sherif [ITCS, 2023] to handle tree-like affine DAGs. We introduce additional ideas from linear algebra to handle forget nodes along long paths.Fri, 06 Sep 2024 21:57:56 +0300https://eccc.weizmann.ac.il/report/2024/132