ECCC
Electronic Colloquium on Computational Complexity
Login | Register | Classic Style



REPORTS > DETAIL:

Revision(s):

Revision #3 to TR01-103 | 23rd August 2002 00:00

Complexity of semi-algebraic proofs Revision of: TR01-103

RSS-Feed




Revision #3
Authors: Dima Grigoriev, Edward Hirsch, Dmitrii V. Pasechnik
Accepted on: 23rd August 2002 00:00
Downloads: 984
Keywords: 


Abstract:


It is a known approach to translate propositional formulas into
systems of polynomial inequalities and to consider proof systems
for the latter ones. The well-studied proof systems of this kind
are the Cutting Planes proof system (CP) utilizing linear
inequalities and the Lovasz-Schrijver calculi (LS) utilizing
quadratic inequalities. We introduce generalizations LS^d of LS
that operate with polynomial inequalities of degree at most d.

It turns out that the obtained proof systems are very strong. We
construct polynomial-size bounded degree LS^d proofs of the
clique-coloring tautologies (which have no polynomial-size CP
proofs), the symmetric knapsack problem (which has no bounded
degree Positivstellensatz Calculus proofs), and Tseitin's
tautologies (which are hard for many known proof systems).
Extending our systems with a division rule yields a polynomial
simulation of CP with polynomially bounded coefficients, while
other extra rules further reduce the proof degrees for the
aforementioned examples.

Finally, we prove lower bounds on Lovasz-Schrijver ranks and on
the "Boolean degree" of Positivstellensatz Calculus refutations.
We use the latter bound to obtain an exponential lower bound on
the size of static LS^d refutations.

This revision contains a proof of exponential lower bound on the
size of Positivstellensatz Calculus refutations as well.


Revision #2 to TR01-103 | 23rd April 2002 00:00

Complexity of semi-algebraic proofs Revision of: TR01-103





Revision #2
Authors: Dima Grigoriev, Edward Hirsch, Dmitrii V. Pasechnik
Accepted on: 23rd April 2002 00:00
Downloads: 937
Keywords: 


Abstract:

It is a known approach to translate propositional formulas into
systems of polynomial inequalities and to consider proof systems
for the latter ones. The well-studied proof systems of this kind
are the Cutting Planes proof system (CP) utilizing linear
inequalities and the Lovasz-Schrijver calculi (LS) utilizing
quadratic inequalities. We introduce generalizations LS^d of LS
that operate with polynomial inequalities of degree at most d.

It turns out that the obtained proof systems are very strong. We
construct polynomial-size bounded degree LS^d proofs of the
clique-coloring tautologies (which have no polynomial-size CP
proofs), the symmetric knapsack problem (which has no bounded
degree Positivstellensatz Calculus proofs), and Tseitin's
tautologies (which are hard for many known proof systems).
Extending our systems with a division rule yields a polynomial
simulation of CP with polynomially bounded coefficients, while
other extra rules further reduce the proof degrees for the
aforementioned examples.

Finally, we prove lower bounds on Lovasz-Schrijver ranks and on
the "Boolean degree" of Positivstellensatz Calculus refutations.
We use the latter bound to obtain an exponential lower bound on
the size of static LS^d refutations.

This revision contains a shorter self-contained proof of Theorem 8.1.
It also fixed typos in Theorem 3.1 and Lemma 8.2 of Revision 1.


Revision #1 to TR01-103 | 8th April 2002 00:00

Complexity of semi-algebraic proofs Revision of: TR01-103





Revision #1
Authors: Dima Grigoriev, Edward Hirsch, Dmitrii V. Pasechnik
Accepted on: 8th April 2002 00:00
Downloads: 940
Keywords: 


Abstract:

It is a known approach to translate propositional formulas into
systems of polynomial inequalities and to consider proof systems
for the latter ones. The well-studied proof systems of this kind
are the Cutting Planes proof system (CP) utilizing linear
inequalities and the Lovasz-Schrijver calculi (LS) utilizing
quadratic inequalities. We introduce generalizations LS^d of LS
that operate with polynomial inequalities of degree at most d.

It turns out that the obtained proof systems are very strong. We
construct polynomial-size bounded degree LS^d proofs of the
clique-coloring tautologies (which have no polynomial-size CP
proofs), the symmetric knapsack problem (which has no bounded
degree Positivstellensatz Calculus proofs), and Tseitin's
tautologies (which are hard for many known proof systems).
Extending our systems with a division rule yields a polynomial
simulation of CP with polynomially bounded coefficients, while
other extra rules further reduce the proof degrees for the
aforementioned examples.

Finally, we prove lower bounds on Lovasz-Schrijver ranks and on
the "Boolean degree" of Positivstellensatz Calculus refutations.
We use the latter bound to obtain an exponential lower bound on
the size of static LS^d and tree-like LS^d refutations.

This revision contains a shorter self-contained proof of Theorem 8.1.


Paper:

TR01-103 | 14th December 2001 00:00

Complexity of semi-algebraic proofs





TR01-103
Authors: Dima Grigoriev, Edward Hirsch, Dmitrii V. Pasechnik
Publication: 22nd December 2001 18:09
Downloads: 804
Keywords: 


Abstract:

It is a known approach to translate propositional formulas into
systems of polynomial inequalities and to consider proof systems
for the latter ones. The well-studied proof systems of this kind
are the Cutting Planes proof system (CP) utilizing linear
inequalities and the Lovasz-Schrijver calculi (LS) utilizing
quadratic inequalities. We introduce generalizations LS^d of LS
that operate with polynomial inequalities of degree at most d.

It turns out that the obtained proof systems are very strong. We
construct polynomial-size bounded degree LS^d proofs of the
clique-coloring tautologies (which have no polynomial-size CP
proofs), the symmetric knapsack problem (which has no bounded
degree Positivstellensatz Calculus proofs), and Tseitin's
tautologies (which are hard for many known proof systems).
Extending our systems with a division rule yields a polynomial
simulation of CP with polynomially bounded coefficients, while
other extra rules further reduce the proof degrees for the
aforementioned examples.

Finally, we prove lower bounds on Lovasz-Schrijver ranks and on
the "Boolean degree" of Positivstellensatz Calculus refutations.
We use the latter bound to obtain an exponential lower bound on
the size of static LS^d refutations.



ISSN 1433-8092 | Imprint