__
TR20-034 | 12th March 2020 14:28
__

#### On Proof complexity of Resolution over Polynomial Calculus

**Abstract:**
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.