ECCC-Report TR20-034https://eccc.weizmann.ac.il/report/2020/034Comments and Revisions published for TR20-034en-usMon, 20 Apr 2020 20:07:26 +0300
Revision 1
| On Proof complexity of Resolution over Polynomial Calculus |
Erfan Khaniki
https://eccc.weizmann.ac.il/report/2020/034#revision1 The refutation system ${Res}_R({PC}_d)$ is a natural extension of resolution refutation system such that it operates with disjunctions of degree $d$ polynomials over ring $R$ with boolean variables. For $d=1$, this system is called ${Res}_R({lin})$. Based on properties of $R$, ${Res}_R({lin})$ systems can be too strong to prove lower bounds for CNFs with current methods. The reachable goal might be proving lower bounds for ${Res}_R({lin})$ when $R$ is a finite field such as $\mathbb{F}_2$. Interestingly, ${Res}_{\mathbb{F}_2}({lin})$ is also fairly strong, and there is no known nontrivial lower bound for it, but for ${Res}^*_R({lin})$ (tree-like ${Res}_R({lin})$) we know exponential lower bounds for every finite field.
For the stronger systems ${Res}_R({PC}_d)$ and ${Res}_R^*({PC}_d)$ for $d>1$ on finite ring $R$, there is no known lower bounds till now. In this paper we will investigate these refutation systems and make some progress toward understanding these systems, including the case $d=1$. We prove a size-width relation for ${Res}_R({PC}_d)$ and ${Res}^*_R({PC}_d)$ for every finite ring $R$. This relation is proved by a new idea to reduce the problem to the original Ben-Sasson and Wigderson size-width relation for ${Res}$ and ${Res}^*$ using extension variables. As a by product, we get the following new lower bounds for every finite field $\mathbb{F}$:
(1) We prove the first nontrivial lower bounds for ${Res}_\mathbb{F}({PC}_d)$ for fixed $d$: a nearly quadratic lower bounds for:
(a) mod $q$ Tseitin formulas ($char(\F)\neq q$),
(b) Random $k$-CNFs with linearly many clauses.
(2) We also prove superpolynomial and exponential lower bounds for ${Res}^*_\mathbb{F}({PC}_{d})$ where $d$ is not too large with respect to $n$ for the following principles:
(a) mod $q$ Tseitin formulas ($char(\mathbb{F})\neq q$),
(b) Random $k$-CNFs.Mon, 20 Apr 2020 20:07:26 +0300https://eccc.weizmann.ac.il/report/2020/034#revision1
Paper TR20-034
| On Proof complexity of Resolution over Polynomial Calculus |
Erfan Khaniki
https://eccc.weizmann.ac.il/report/2020/034 The refutation system ${Res}_R({PC}_d)$ is a natural extension of resolution refutation system such that it operates with disjunctions of degree $d$ polynomials over ring $R$ with boolean variables. For $d=1$, this system is called ${Res}_R({lin})$. Based on properties of $R$, ${Res}_R({lin})$ systems can be too strong to prove lower bounds for CNFs with current methods. The reachable goal might be proving lower bounds for ${Res}_R({lin})$ when $R$ is a finite field such as $\mathbb{F}_2$. Interestingly, ${Res}_{\mathbb{F}_2}({lin})$ is also fairly strong, and there is no known nontrivial lower bound for it, but for ${Res}^*_R({lin})$ (tree-like ${Res}_R({lin})$) we know exponential lower bounds for every finite field.
For the stronger systems ${Res}_R({PC}_d)$ and ${Res}_R^*({PC}_d)$ for $d>1$ on finite ring $R$, there is no known lower bounds till now. In this paper we will investigate these refutation systems and make some progress toward understanding these systems, including the case $d=1$. We prove a size-width relation for ${Res}_R({PC}_d)$ and ${Res}^*_R({PC}_d)$ for every finite ring $R$. This relation is proved by a new idea to reduce the problem to the original Ben-Sasson and Wigderson size-width relation for ${Res}$ and ${Res}^*$ using extension variables. As a by product, we get the following new lower bounds for every finite field $\mathbb{F}$:
(1) We prove the first nontrivial lower bounds for ${Res}_\mathbb{F}({PC}_d)$ for fixed $d$: a nearly quadratic lower bounds for mod $q$ Tseitin formulas ($char(\mathbb{F})\neq q$) for suitable graphs.
(2) We also prove superpolynomial and exponential lower bounds for ${Res}^*_\mathbb{F}({PC}_{d})$ where $d$ is not too large with respect to $n$ for the following principles:
(a) mod $q$ Tseitin formulas ($char(\mathbb{F})\neq q$),
(b) Random $k$-CNFs.Fri, 13 Mar 2020 17:56:30 +0200https://eccc.weizmann.ac.il/report/2020/034