Результаты исследований: Публикации в книгах, отчётах, сборниках, трудах конференций › статья в сборнике материалов конференции › научная › Рецензирование
Complexity of semi-algebraic proofs. / Grigoriev, Dima; Hirsch, Edward A.; Pasechnik, Dmitrii V.
STACS 2002 - 19th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings. ред. / Afonso Ferreira; Helmut Alt. Springer Nature, 2002. стр. 419-430 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Том 2285).Результаты исследований: Публикации в книгах, отчётах, сборниках, трудах конференций › статья в сборнике материалов конференции › научная › Рецензирование
}
TY - GEN
T1 - Complexity of semi-algebraic proofs
AU - Grigoriev, Dima
AU - Hirsch, Edward A.
AU - Pasechnik, Dmitrii V.
PY - 2002/1/1
Y1 - 2002/1/1
N2 - Proof systems for polynomial inequalities in 0-1 variables include the well-studied Cutting Planes proof system (CP) and the Lov´asz-Schrijver calculi (LS) utilizing linear, respectively, quadratic, inequalities. We introduce generalizations LSd of LSinvolving 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´asz-Schrijver ranks, demonstrating, in particular, their rather limited applicability for proof complexity.
AB - Proof systems for polynomial inequalities in 0-1 variables include the well-studied Cutting Planes proof system (CP) and the Lov´asz-Schrijver calculi (LS) utilizing linear, respectively, quadratic, inequalities. We introduce generalizations LSd of LSinvolving 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´asz-Schrijver ranks, demonstrating, in particular, their rather limited applicability for proof complexity.
UR - http://www.scopus.com/inward/record.url?scp=84937409644&partnerID=8YFLogxK
M3 - Conference contribution
AN - SCOPUS:84937409644
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 419
EP - 430
BT - STACS 2002 - 19th Annual Symposium on Theoretical Aspects of Computer Science, Proceedings
A2 - Ferreira, Afonso
A2 - Alt, Helmut
PB - Springer Nature
T2 - 19th Annual Symposium on Theoretical Aspects of Computer Science, STACS 2002
Y2 - 14 March 2002 through 16 March 2002
ER -
ID: 49828970