Abstract
The proof system $Res(PC_{d,R})$ is a natural extension of the Resolution proof system that instead of disjunctions of literals operates with disjunctions of degree $d$ multivariate polynomials over a ring $R$ with Boolean variables. Proving super-polynomial lower bounds for the size of $Res(PC_{1,R})$-refutations of CNFs is one of the important problems in propositional proof complexity. The existence of such lower bounds is even open for $Res(PC_{1,F})$ when $F$ is a finite field such as $F_2$. In this talk, we prove size-width relations for $Res(PC_{d,R})$ and tree-like $Res(PC_{d,R}) when $R$ is a finite ring. Using these size-width relations, we prove new lower bounds and also reprove some known lower bounds for (tree-like) $Res(PC_{d,F})$ when $F$ is a finite field. In particular, we prove almost quadratic lower bounds for $Res(Lin_{F_2})$ ($Res(PC_{1,F_2})$) for Mod $q$ Tseitin formulas and random $k$-CNFs.