ABSTRACT. We study the complexity of resolution extended with the ability to count over different characteristics and rings. These systems capture integer and moduli counting, and in particular admit short tree-like refutations for insolvable sets of linear equations. For this purpose, we consider the system ResLin(R), in which proof-lines are disjunction of linear equations over a ring R.(We focus on the case where the variables are Boolean, i.e., we add the Boolean axioms (x=0)\/(x=1), for all variables x.) Extending the work of Itsykson and Sokolov we obtain new lower bounds and separations, as follows:

Finite fields:

Exponential-size lower bounds for tree-like ResLin(Fp) refutations of Tseitin mod q formulas, for every pair of distinct primes p,q. As a corollary we obtain an exponential-size separation between tree-like ResLin(Fp) and tree-like ResLin(Fq).

Exponential-size lower bounds for tree-like ResLin(Fp) refutations of random k-CNF formulas, for every prime p and constant k.

Exponential-size lower bounds for tree-like ResLin(F) refutations of the pigeonhole principle, for every field F.

All the above hard instances are encoded as CNF formulas. The lower bounds are proved using extensions and modifications of the Prover-Delayer game technique and size-width relations.

Characteristic zero fields:

Separation of tree-like ResLin(F) and (dag-like) ResLin(F), for characteristic zero fields F. The separating instances are the pigeonhole principle and the Subset Sum principle. The latter is the formula a1 x1 +... +an xn = b, for some b not in the image of the linear form. The lower bound for the Subset Sum principle employs the notion of immunity from Alekhnovich and Razborov.