Ricerc@Sapienza

We show that if a k-CNF requires width w to refute in resolution, then it requires space square root of √ω to refute in polynomial calculus, where the space of a polynomial calculus refutation is the number of monomials that must be kept in memory when working through the proof. This is the first analogue, in polynomial calculus, of Atserias and Dalmau's result lower-bounding clause space in resolution by resolution width.

We investigate the space complexity of refuting 3-CNFs in Resolution and algebraic systems. We prove that every Polynomial Calculus with Resolution refutation of a random 3-CNF ? in n variables requires, with high probability, distinct monomials to be kept simultaneously in memory. The same construction also proves that every Resolution refutation of ? requires, with high probability, clauses each of width to be kept at the same time in memory. This gives a lower bound for the total space needed in Resolution to refute ?.