TR18-117 Authors: Fedor Part, Iddo Tzameret

Publication: 23rd June 2018 17:07

Downloads: 171

Keywords:

Resolution over linear equations (introduced in [RT08]) emerged recently as an important object of study. This refutation system, denoted Res(lin$_R$), operates with disjunction of linear equations over a ring $R$. On the one hand, the system captures a natural ``minimal'' extension of resolution in which efficient counting can be achieved; while on the other hand, as observed by, e.g., Krajicek [Kra16] (cf. [IS14,KO18,GK17]), when considered over prime fields, and specifically $\mathbf{F}_2$, super-polynomial lower bounds on (dag-like) Res(lin$_{\mathbf{F}_2}$) is a first step towards the long-standing open problem of establishing constant-depth Frege with counting gates (AC$^0[2]$-Frege) lower bounds.

In this work we develop new lower bound techniques for resolution over linear equations and extend existing ones to work over different rings. We obtain a host of new lower bounds, separations and upper bounds, while calibrating the relative strength of different sub-systems. We first establish, over fields of characteristic zero, exponential-size *dag-like* lower bounds against resolution over linear equations refutations of instances with large coefficients. Specifically, we demonstrate that the subset sum principle $\alpha_1 x_1 +\ldots +\alpha_n x_n = \beta$, for $\beta$ not in the image of the linear form, requires refutations proportional to the size of the image. Moreover, for instances with small coefficients, we separate the tree and dag-like versions of Res(lin$_{\mathbf{F}}$), when $\mathbf{F}$ is of characteristic zero, by employing the notion of immunity from Alekhnovich-Razborov [AR01], among other techniques.

We then study resolution over linear equations over different *finite* fields, extending the work of Itsykson and Sokolov [IS14] who developed tree-like Res(lin$_{\mathbf{F}_2}$) lower bounds techniques. We obtain new lower bounds and separations as follows: (i) exponential-size lower bounds for tree-like Res(lin$_{\mathbf{F}_p}$) Tseitin mod $q$ formulas, for every pair of distinct primes $p, q$. As a corollary we obtain an exponential-size separation between tree-like Res(lin$_{\mathbf{F}_p}$) and tree-like Res(lin$_{\mathbf{F}_q}$); (ii) exponential-size lower bounds for tree-like Res(lin$_{\mathbf{F}_p}$) refutations of random $k$-CNF formulas, for every prime $p$ and constant $k$; and (iii) exponential-size lower bounds for tree-like Res(lin$_{\mathbf{F}}$) refutations of the pigeonhole principle, for *every* field $\mathbf{F}$.