Name
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 Ω(&sqrt; 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. |
Year | DOI | Venue |
|---|---|---|
2010 | 10.1145/1838552.1838556 | ACM Trans. Comput. Log. |
Keywords | Field | DocType |
pcr refutation,tradeoff optimality,algebraic proofs,polynomial calculus,previous degree,polynomial encoding,short refutation,algebraic proof system pcrk,computational complexity,conjunctive normal form,low degree,size-degree tradeoffs,proof complexity,k-dnf resolution,lower bound | Discrete mathematics,Combinatorics,Algebraic number,Polynomial,Upper and lower bounds,Conjunctive normal form,Proof complexity,Mathematics,Encoding (memory),Computational complexity theory,Exponential growth | Journal |
Volume | Issue | ISSN |
12 | 1 | 1529-3785 |
Citations | PageRank | References |
12 | 0.49 | 21 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Nicola Galesi | 1 | 367 | 28.05 |
| Massimo Lauria | 2 | 122 | 14.73 |