Revision #1 Authors: Fedor Part, Iddo Tzameret

Accepted on: 20th February 2019 12:43

Downloads: 94

Keywords:

Resolution over linear equations (Raz and Tzameret 2008) is a natural extension of resolution augmented with the ability to carry out basic counting. Denoted Res(lin$_R$), this refutation system operates with disjunctions of linear equations (with 0-1 variables) over a ring $R$ to refute unsatisfiable propositional formulas. As observed recently by, e.g., Krajicek (2017) (cf. [IS14, KO18, GK18]), Res(lin$_R$) captures a “minimal” extension of resolution with counting gates for which no (general, that is, dag-like) super-polynomial lower bounds are known to date.

In this work we develop new lower bound techniques for resolution over linear equations and extend existing ones. We obtain a host of new lower bounds, separations and upper bounds, while calibrating the relative strength of different sub-systems. In particular, we establish the first known exponential-size *dag-like* lower bound against resolution over linear equations refutations: we demonstrate

that the Subset Sum principle $\alpha_1 x_1 +\cdots +\alpha_n x_n = \beta$ for $\beta$ not in the image of the linear form (under 0-1 assignments), requires refutations proportional to the size of the image. This leads to exponential lower bounds when the field (as well as the image) are sufficiently large. Taking this idea further, based on the image of a generator matrix of a linear error-correcting code, we propose a hard candidate for dag-like Res(lin$_R$) refutations over finite fields. As a modest step towards dag-like lower bounds over finite fields we establish a strong lower bound against restricted

tree-like refutations for this hard candidate. Moreover, we separate the tree and dag-like versions of Res(lin$_R$), when $\mathbb{F}$ is of characteristic zero, by employing (among others) the notion of immunity from Alekhnovich-Razborov (2001).

Turning to tree-like refutations over finite fields, we extend the work of Itsykson and Sokolov (2014) who obtained lower bounds over $\mathbb{F}_2$. We establish new lower bounds and separations as follows: (i) for every pair of distinct primes $p, q$, there exist CNF formulas with short tree-like refutations in Res(lin$_{\mathbb{F}_p}$) that require exponential-size tree-like Res(lin$_{\mathbb{F}_q}$) refutations; (ii) random $k$-CNF formulas require exponential-size tree-like Res(lin$_{\mathbb{F}_p}$) refutations, for every prime $p$ and constant $k$; and (iii) exponential-size lower bounds for tree-like Res(lin$_{\mathbb{F}}$) refutations

of the pigeonhole principle, for every field $\mathbb{F}$.

1. Added a hard candidate for dag-like resolution over linear equations for finite fields, and proved a restricted lower bound for this candidate (based on Gilbert bound for error correcting codes).

2. Some minor improvements and modifications to the exposition.

TR18-117 Authors: Fedor Part, Iddo Tzameret

Publication: 23rd June 2018 17:07

Downloads: 292

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}$.