|Title||Random CNF’s are Hard for the Polynomial Calculus|
|Author(s)|| Eli Ben-Sasson, Russell Impagliazzo|
|Type||Article in Journal|
|Abstract||We prove linear lower bounds on the Polynomial Calculus (PC) refutation-degree of random CNF whenever the underlying field has characteristic greater than 2. Our proof follows by showing the PC refutation-degree of a unsatisfiable system of linear equations modulo 2 is equivalent to its Gaussian width, a concept defined by the late Mikhail Alekhnovich.|
The equivalence of refutation-degree and Gaussian width which is the main contribution of this paper, allows us to also simplify the refutation-degree lower bounds of Buss et al. (2001) and additionally prove non-trivial upper bounds on the resolution and PC complexity of refuting unsatisfiable systems of linear equations.
|Keywords||Propositional proof complexity, polynomial calculus, Groebner basis, random CNF formulae|
|Publisher||Springer (Birkh\"auser), Basel|