Proof systems for polynomial inequalities in 0-1 variables include the well-studied
Cutting Planes proof system (CP) and the
Lovász- Schrijver calculi (LS) utilizing linear, respectively, quadratic, inequalities. We introduce generalizations LS
d of LS involving polynomial inequalities of degree at most
d.
Surprisingly, the systems LSd turn out to be very strong. We construct polynomial-size bounded degree LSd proofs of the clique-coloring tautologies (which have no polynomial-size CP proofs), the symmetric knapsack problem (which has no bounded degree Positivstellensatz Calculus (PC) proofs), and Tseitin’s tautologies (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 Lovász-Schrijver ranks, demonstrating, in particular, their rather limited applicability for proof complexity.
Due to the space considerations we had to shorten this text rather drastically. For the full version, that also contains new
results not mentioned here, the reader is referred to [1].
A part of this work was completed while visiting Delft University of Technology. Partially supported by grant #1 of the 6th
RAScon test-expertise of young scientists projects (1999) and a grant from NATO.