Abstract
Resolution over linear equations 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 the work of [Ran Raz and Iddo Tzameret, 2008], through the work of [Dmitry Itsykson and Dmitry Sokolov, 2014] which focused on treelike lower bounds, this refutation system was shown to be fairly strong. Subsequent work (cf. [Jan Krajícek, 2017; Dmitry Itsykson and Dmitry Sokolov, 2014; Jan Krajícek and Igor Carboni Oliveira, 2018; Michal Garlik and Lezsek Kołodziejczyk, 2018]) 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 superpolynomial lower bounds are known to date.
We provide the first superpolynomial size lower bounds on general (daglike) resolution over linear equations refutations in the large characteristic regime. In particular we prove that the subsetsum principle 1+ x_1 + ̇s +2^n x_n = 0 requires refutations of exponentialsize over ℚ. Our proof technique is nontrivial and novel: roughly speaking, we show that under certain conditions every refutation of a subsetsum instance f=0, where f is a linear polynomial over ℚ, must pass through a fat clause containing an equation f=α for each α in the image of f under boolean assignments. We develop a somewhat different approach to prove exponential lower bounds against treelike refutations of any subsetsum instance that depends on n variables, hence also separating treelike from daglike refutations over the rationals.
We then turn to the finite fields regime, showing that the work of Itsykson and Sokolov [Dmitry Itsykson and Dmitry Sokolov, 2014] who obtained treelike lower bounds over 𝔽_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 treelike refutations in Res(lin_{𝔽_p}) that require exponentialsize treelike Res(lin_{𝔽_q}) refutations; (ii) random kCNF formulas require exponentialsize treelike Res(lin_{𝔽_p}) refutations, for every prime p and constant k; and (iii) exponentialsize lower bounds for treelike Res(lin_𝔽) refutations of the pigeonhole principle, for every field 𝔽.
BibTeX  Entry
@InProceedings{part_et_al:LIPIcs:2020:11704,
author = {Fedor Part and Iddo Tzameret},
title = {{Resolution with Counting: DagLike Lower Bounds and Different Moduli}},
booktitle = {11th Innovations in Theoretical Computer Science Conference (ITCS 2020)},
pages = {19:119:37},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959771344},
ISSN = {18688969},
year = {2020},
volume = {151},
editor = {Thomas Vidick},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/11704},
URN = {urn:nbn:de:0030drops117041},
doi = {10.4230/LIPIcs.ITCS.2020.19},
annote = {Keywords: Proof complexity, concrete lower bounds, resolution, satisfiability, combinatorics}
}
Keywords: 

Proof complexity, concrete lower bounds, resolution, satisfiability, combinatorics 
Collection: 

11th Innovations in Theoretical Computer Science Conference (ITCS 2020) 
Issue Date: 

2020 
Date of publication: 

06.01.2020 