This paper gives nearly optimal lower bounds on the minimum degree of polynomial calculus refutations of Tseitin's graph tautologies and the mod P 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 Grobner basis algorithm used as a heuristic for k-SAT, requires exponen- tial time in the worst case.
展开▼
