Weizmann Logo
ECCC
Electronic Colloquium on Computational Complexity

Under the auspices of the Computational Complexity Foundation (CCF)

Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #1 to TR07-041 | 16th November 2007 00:00

Extending Polynomial Calculus with $k$-DNF Resolution

RSS-Feed




Revision #1
Authors: Nicola Galesi, Massimo Lauria
Accepted on: 16th November 2007 00:00
Downloads: 2866
Keywords: 


Abstract:

We consider two well-known algebraic proof systems: Polynomial Calculus (Pc) and Polynomial Calculus with Resolution (Pcr), a system introduced in \cite{abrw02j} which combines together Pc and Resolution.

Moreover we introduce an algebraic proof system Pcr{k}, which combines together Polynomial Calculus Pc and k-DNF Resolution (Res{k}).
This is a natural generalization to Res{k} of Pcr.

In the paper we study the complexity of proofs in such systems.

First we prove that a set of polynomials encoding a Graph Ordering Principle (Gop(G)) requires Pcr refutations of degree $\Omega(n)$. This is the first linear degree lower bound for \Pcr\ refutations for ordering principles. This result immediately implies that the size-degree tradeoff for Pcr Refutations of Alekhnovich et al. \cite{abrw04j} is optimal, since there are polynomial size Pcr refutations for Gop(G).

We then study the complexity of proofs in Pcr{k}, extending to these systems the lower bounds known for Res{k}:
- we prove that random $3$-CNF formulas with a linear number of clauses are hard to prove in Pcr{k} (over a field with characteristic different from $2$) as long as $k$ is in $o(\sqrt{\log n/\log \log n})$. This is the strongest daglike system where $3$-CNF formulas are hard to prove.
- Moreover we prove a strict hierarchy result showing that \Pcrk{k+1} is
exponentially stronger than Pcr{k}.


Paper:

TR07-041 | 20th April 2007 00:00

Extending Polynomial Calculus to $k$-DNF Resolution





TR07-041
Authors: Nicola Galesi, Massimo Lauria
Publication: 3rd May 2007 17:50
Downloads: 3001
Keywords: 


Abstract:

We introduce an algebraic proof system Pcrk, which combines together {\em Polynomial Calculus} (Pc) and {\em $k$-DNF Resolution} (Resk).
This is a natural generalization to Resk of the well-known {\em Polynomial Calculus with Resolution} (Pcr) system which combines together Pc and Resolution.

We study the complexity of proofs in such a system extending to Pcrk the results known for Resk. We prove that random 3-CNF formulas with a linear number of clauses are hard to prove in Pcrk (over a field with characteristic different from 2) as long as k is in $o(\sqrt{\log n/\log \log n})$. This is the strongest system where 3-CNF formulas are hard to prove.

Moreover we prove a strict hierarchy result showing that Pcr(k+1) is exponentially stronger than Pcrk. This result is the consequence of proving a $\Omega(n)$ degree lower bound for Pcr refutations of a {\em Graph Ordering Principle}. This is the first example of a family of contradictions having Pcr short refutations but requiring high degree, and thus also proving the optimality of the size-degree tradeoff for Pcr.



ISSN 1433-8092 | Imprint