ECCC-Report TR01-103https://eccc.weizmann.ac.il/report/2001/103Comments and Revisions published for TR01-103en-usFri, 23 Aug 2002 00:00:00 +0300
Revision 3
| Complexity of semi-algebraic proofs Revision of: TR01-103 |
Dima Grigoriev,
Edward Hirsch,
Dmitrii V. Pasechnik
https://eccc.weizmann.ac.il/report/2001/103#revision3
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.
Fri, 23 Aug 2002 00:00:00 +0300https://eccc.weizmann.ac.il/report/2001/103#revision3
Revision 2
| Complexity of semi-algebraic proofs Revision of: TR01-103 |
Dima Grigoriev,
Edward Hirsch,
Dmitrii V. Pasechnik
https://eccc.weizmann.ac.il/report/2001/103#revision2It 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.
Tue, 23 Apr 2002 00:00:00 +0300https://eccc.weizmann.ac.il/report/2001/103#revision2
Revision 1
| Complexity of semi-algebraic proofs Revision of: TR01-103 |
Dima Grigoriev,
Edward Hirsch,
Dmitrii V. Pasechnik
https://eccc.weizmann.ac.il/report/2001/103#revision1It 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.
Mon, 08 Apr 2002 00:00:00 +0300https://eccc.weizmann.ac.il/report/2001/103#revision1
Paper TR01-103
| Complexity of semi-algebraic proofs |
Dima Grigoriev,
Edward Hirsch,
Dmitrii V. Pasechnik
https://eccc.weizmann.ac.il/report/2001/103It 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.
Sat, 22 Dec 2001 18:09:52 +0200https://eccc.weizmann.ac.il/report/2001/103