Random CNFs are hard for the polynomial calculus
Eli Ben‐Sasson, Russell Impagliazzo · 2003
We show a general reduction that derives lower bounds on degrees of polynomial calculus proofs of tautologies, over any field of characteristic (other than 2) from lower bounds for resolution proofs of a related set of linear equations module 2. We apply this to derive linear lower bounds on the degrees of PC proofs of randomly generated tautologies.