Random Cnf's are Hard for the Polynomial Calculus

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 modulo 2. We apply this to derive linear lower bounds on the degrees of PC proofs of randomly generated tautologies.

• Type: Journal
• Year: 2010
• Where: CC
• Authors: Eli Ben-Sasson, Russell Impagliazzo
• Keywords: CC 2010, Lower Bounds, Polynomial Calculus Proofs, Resolution Proofs, System Software