Revision #3 Authors: Dima Grigoriev, Edward Hirsch, Dmitrii V. Pasechnik

Accepted on: 23rd August 2002 00:00

Downloads: 984

Keywords:

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 Authors: Dima Grigoriev, Edward Hirsch, Dmitrii V. Pasechnik

Accepted on: 23rd April 2002 00:00

Downloads: 937

Keywords:

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 Authors: Dima Grigoriev, Edward Hirsch, Dmitrii V. Pasechnik

Accepted on: 8th April 2002 00:00

Downloads: 940

Keywords:

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.

TR01-103 Authors: Dima Grigoriev, Edward Hirsch, Dmitrii V. Pasechnik

Publication: 22nd December 2001 18:09

Downloads: 804

Keywords:

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.

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.