Optimality of size-degree tradeoffs for polynomial calculus

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 PcRk which combines together polynomial calculus and k-DNF resolution (RESk). We show a size hierarchy theorem for PCRk:PCRk is exponentially separated from PCRk+1. This follows from the previous degree lower bound and from techniques developed for RESk. Finally we show that random formulas in conjunctive normal form (3-CNF) are hard to refute in PcRk. © 2010 ACM.