Optimality of size-degree tradeoffs for polynomial calculus

Abstract

There are methods to turn short refutations in polynomial calculus (Pc) and polynomial calculus with resolution (Pcr) into refutations of low degree. Bonet and Galesi [1999, 2003] asked if such size-degree tradeoffs for Pc [Clegg et al. 1996; Impagliazzo et al. 1999] and Pcr [Alekhnovich et al. 2004] are optimal. We answer this question by showing a polynomial encoding of the graph ordering principle on m variables which requires Pc and Pcr refutations of degree Ω(√ m ). Tradeoff optimality follows from our result and from the short refutations of the graph ordering principle in Bonet and Galesi [1999, 2001]. We then introduce the algebraic proof system Pcr k which combines together polynomial calculus and k-DNF resolution (Res k ). We show a size hierarchy theorem for Pcr k : Pcr k is exponentially separated from Pcr k+1 . This follows from the previous degree lower bound and from techniques developed for Res k . Finally we show that random formulas in conjunctive normal form (3-CNF) are hard to refute in Pcr k .