查看文章

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 LSd 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 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 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 coe cients, while other extra rules further reduce the proof degrees for the aforementioned examples. Finally, we prove lower bounds on Lov asz-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 LSd and tree-like LSd refutations.