Resolution over linear equations introduced in (Raz & Tzameret 2008) is a natural extension of the popular resolution refutation system, augmented with the ability to carry out basic counting. Denoted Res(lin$_R$), this refutation system operates with disjunctions of linear equations with boolean variables over a ring $R$, to refute unsatisfiable sets of such disjunctions. Beginning in (Raz \& Tzameret 2008), through the work of (Itsykson & Sokolov 2020)} which focused on tree-like lower bounds, this refutation system was shown to be fairly strong. Subsequent work (cf.~[Kra16,IS14,KO18,GK17]) made it evident that establishing lower bounds against general Res(lin$_R$) refutations is a challenging and interesting task since the system captures a ``minimal'' extension of resolution with counting gates for which no super-polynomial lower bounds are known to date.

We provide the first super-polynomial size lower bounds against general (dag-like) resolution over linear equations refutations in the large characteristic regime. In particular we prove that the subset-sum principle $1+\sum\limits_{i=1}^{n}2^i x_i = 0$ requires refutations of exponential-size over $\mathbb{Q}$. We use a novel lower bound technique: we show that under certain conditions every refutation of a subset-sum instance $f=0$ must pass through a fat clause consisting of the equation $f=\alpha$ for every $\alpha$ in the image of $f$ under boolean assignments, or can be efficiently reduced to a proof containing such a clause. We then modify this approach to prove exponential lower bounds against tree-like refutations of any subset-sum instance that depends on $n$ variables, hence also separating tree-like from dag-like refutations over the rationals.

We then turn to the finite fields regime, showing that the work of (Itsykson and Sokolov 2014) who obtained tree-like lower bounds over $\mathbf{F}_2$ can be carried over and extended to every finite field. 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$_{\mathbf{F}_p}$) that require exponential-size tree-like Res(lin$_{\mathbf{F}_q}$) refutations; (ii) random $k$-CNF formulas require exponential-size tree-like Res(lin$_{\mathbf{F}_p}$) refutations, 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}$.

1- Improved overall exposition.
2- Improved exposition of the dag-like lower bound proof.
3- Other minor fixes and additions of details to some proofs.

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.

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