|
This article is cited in 35 scientific papers (total in 35 papers)
Complexity of semialgebraic proofs
D. Yu. Grigor'eva, E. A. Hirschb, D. V. Pasechnikcd a University of Rennes 1
b St. Petersburg Department of V. A. Steklov Institute of Mathematics, Russian Academy of Sciences
c Delft University of Technology
d Johann Wolfgang Goethe-Universität
Abstract:
It is a known approach to translate propositional formulas into systems of polynomial inequalities and consider proof systems for the latter. The well-studied proof systems of this type are the Cutting Plane proof system (CP) utilizing linear inequalities and the Lovász–Schrijver calculi (LS) utilizing quadratic inequalities. We introduce generalizations ${\rm LS}^d$ of LS that operate on polynomial inequalities of degree at mos $d$.
It turns out that the obtained proof systems are very strong. We construct polynomial-size bounded-degree ${\rm 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 those examples.
Finally, we prove lower bounds on the Lovász–Schrijver ranks and on the size and the “Boolean degree” of Positivstellensatz calculus refutations. We use the latter bound to obtain an exponential lower bound on the size of Positivstellensatz calculus, textit{static} ${\rm LS}^d$, and tree-like ${\rm LS}^d$ refutations.
Key words and phrases:
Computational complexity, propositional proof system.
Received: March 24, 2002
Citation:
D. Yu. Grigor'ev, E. A. Hirsch, D. V. Pasechnik, “Complexity of semialgebraic proofs”, Mosc. Math. J., 2:4 (2002), 647–679
Linking options:
https://www.mathnet.ru/eng/mmj67 https://www.mathnet.ru/eng/mmj/v2/i4/p647
|
Statistics & downloads: |
Abstract page: | 260 | References: | 65 |
|