Resolution with Counting: Lower Bounds over Different Moduli
share
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 F_2, super-polynomial lower bounds on Res(lin_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 lower bounds against resolution over linear equations refutations of instances with large coefficients. Specifically, we demonstrate that the subset sum principle α_1 x_1 +... +α_n x_n = β, for β 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_F), when F is of characteristic zero, by employing the notion of immunity from Alekhnovich-Razborov [AR01], among other techniques. (Abstract continued in the full paper.)
READ FULL TEXT