2026-07-23T15:11:24Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11704 2024-03-06T10:48:30Z ddc:004 open_access

Resolution with Counting: Dag-Like Lower Bounds and Different Moduli Part, Fedor Tzameret, Iddo Proof complexity concrete lower bounds resolution satisfiability combinatorics 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 tree-like 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 super-polynomial lower bounds are known to date. We provide the first super-polynomial size lower bounds on general (dag-like) resolution over linear equations refutations in the large characteristic regime. In particular we prove that the subset-sum principle 1+ x_1 + ̇s +2^n x_n = 0 requires refutations of exponential-size over ℚ. Our proof technique is nontrivial and novel: roughly speaking, we show that under certain conditions every refutation of a subset-sum 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 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 [Dmitry Itsykson and Dmitry Sokolov, 2014] who obtained tree-like 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 tree-like refutations in Res(lin_{?_p}) that require exponential-size tree-like Res(lin_{?_q}) refutations; (ii) random k-CNF formulas require exponential-size tree-like Res(lin_{?_p}) refutations, for every prime p and constant k; and (iii) exponential-size lower bounds for tree-like Res(lin_?) refutations of the pigeonhole principle, for every field ?. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Fedor Part and Iddo Tzameret 2020 Is Part Of LIPIcs, Volume 151, 11th Innovations in Theoretical Computer Science Conference (ITCS 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITCS.2020.19 urn:nbn:de:0030-drops-117041 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2020.19 eng https://creativecommons.org/licenses/by/3.0/legalcode