Linear Gaps between Degrees for the Polynomial Calculus Modulo Distinct Primes

AbstractThis paper gives nearly optimal lower bounds on the minimum degree of polynomial calculus refutations of Tseitin's graph tautologies and the modp counting principles, p⩾2. The lower bounds apply to the polynomial calculus over fields or rings. These are the first linear lower bounds for the polynomial calculus for k-CNF formulas. As a consequence, it follows that the Gröbner basis algorithm used as a heuristic for k-SAT, requires exponential time in the worst case. Moreover, our lower bounds distinguish linearly between proofs over fields of characteristic q and r, q≠r, and more generally distinguish linearly the rings Zq and Zr where q and r do not have the identical prime factors