RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PERSONAL OFFICE
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Mosc. Math. J.:
Year:
Volume:
Issue:
Page:
Find






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


Mosc. Math. J., 2002, Volume 2, Number 4, Pages 647–679 (Mi mmj67)  

This article is cited in 21 scientific papers (total in 21 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 $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 $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} $LS^d$, and tree-like $LS^d$ refutations.

Key words and phrases: Computational complexity, propositional proof system.

Full text: http://www.ams.org/.../abst2-4-2002.html
References: PDF file   HTML file

Bibliographic databases:

MSC: Primary 03F20; Secondary 68Q17
Received: March 24, 2002
Language: English

Citation: D. Yu. Grigor'ev, E. A. Hirsch, D. V. Pasechnik, “Complexity of semialgebraic proofs”, Mosc. Math. J., 2:4 (2002), 647–679

Citation in format AMSBIB
\Bibitem{GriHirPas02}
\by D.~Yu.~Grigor'ev, E.~A.~Hirsch, D.~V.~Pasechnik
\paper Complexity of semialgebraic proofs
\jour Mosc. Math.~J.
\yr 2002
\vol 2
\issue 4
\pages 647--679
\mathnet{http://mi.mathnet.ru/mmj67}
\mathscinet{http://www.ams.org/mathscinet-getitem?mr=1986085}
\zmath{https://zbmath.org/?q=an:1027.03044}


Linking options:
  • http://mi.mathnet.ru/eng/mmj67
  • http://mi.mathnet.ru/eng/mmj/v2/i4/p647

    SHARE: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles

    This publication is cited in the following articles:
    1. Anjos M.F., “On semidefinite programming relaxations for the satisfiability problem”, Math. Methods Oper. Res., 60:3 (2004), 349–367  crossref  mathscinet  zmath  isi
    2. Hirsch E.A., Nikolenko S.I., “Simulating cutting plane proofs with restricted degree of falsity by resolution”, Theory and applications of satisfiability testing, Lecture Notes in Comput. Sci., 3569, Springer, Berlin, 2005, 135–142  crossref  mathscinet  zmath  isi
    3. Anjos M.F., “An improved semidefinite programming relaxation for the satisfiability problem”, Math. Program., 102:3, Ser. A (2005), 589–608  crossref  mathscinet  zmath  isi
    4. D. M. Itsykson, A. A. Kojevnikov, “Lower bounds of static Lovász–Schrijver calculus proofs for Tseitin tautologies”, J. Math. Sci. (N. Y.), 145:3 (2007), 4942–4952  mathnet  crossref  mathscinet  zmath
    5. Anjos M.F., “An explicit semidefinite characterization of satisfiability for Tseitin instances on toroidal grid graphs”, Ann. Math. Artif. Intell., 48:1-2 (2006), 1–14  crossref  mathscinet  zmath  isi
    6. Kojevnikov A., Kulikov A.S., “Complexity of semialgebraic proofs with restricted degree of falsity”, Theory and applications of satisfiability testing—SAT 2006, Lecture Notes in Comput. Sci., 4121, Springer, Berlin, 2006, 11–21  crossref  mathscinet  zmath  isi
    7. Kojevnikov A., Itsykson D., “Lower bounds of static Lovász-Schrijver calculus proofs for Tseitin tautologies”, Automata, languages and programming, Part I, Lecture Notes in Comput. Sci., 4051, Springer, Berlin, 2006, 323–334  crossref  mathscinet  zmath  isi
    8. Hirsch E.A., Kojevnikov A., “Several notes on the power of Gomory-Chvatal cuts”, Ann. Pure Appl. Logic, 141:3 (2006), 429–436  crossref  mathscinet  zmath  isi  elib
    9. Dantchev S., “Rank Complexity Gap for Lovasz-Schrijver and Sherali-Adams Proof Systems”, Stoc 07: Proceedings of the 39th Annual ACM Symposium on Theory of Computing, Annual Acm Symposium on Theory of Computing, 2007, 311–317  mathscinet  zmath  isi
    10. Rhodes M., “Rank lower bounds for the sherali-adams operator”, Computation and Logic in the Real World, Proceedings, Lecture Notes in Computer Science, 4497, 2007, 648–659  crossref  mathscinet  zmath  isi
    11. Rhodes M., “Resolution width and Cutting Plane rank are incomparable”, Mathematical Foundations of Computer Science 2008, Proceedings, Lecture Notes in Computer Science, 5162, 2008, 575–587  crossref  mathscinet  zmath  isi
    12. Rhodes M., “On the Chvatal rank of the Pigeonhole Principle”, Theoret. Comput. Sci., 410:27-29 (2009), 2774–2778  crossref  mathscinet  zmath  isi
    13. Pitassi T., Segerlind N., “Exponential lower bounds and Integrality Gaps for Tree-like Lovasz-Schrijver Procedures”, Proceedings of the Twentieth Annual ACM-SIAM Symposium on Discrete Algorithms, 2009, 355–364  crossref  mathscinet  isi
    14. Mathieu C., Sinclair A., “Sherali-Adams Relaxations of the Matching Polytope”, Stoc'09: Proceedings of the 2009 ACM Symposium on Theory of Computing, 2009, 293–302  crossref  mathscinet  zmath  isi
    15. Pitassi T., Segerlind N., “Exponential Lower Bounds and Integrality Gaps for Tree-Like Lovasz-Schrijver Procedures”, SIAM J Comput, 41:1 (2012), 128–159  crossref  mathscinet  zmath  isi  elib
    16. Dantchev S., Martin B., “Rank Complexity Gap for Lovasz-Schrijver and Sherali-Adams Proof Systems”, Comput. Complex., 22:1 (2013), 191–213  crossref  mathscinet  zmath  isi
    17. Anjos M.F., Vieira M.V.C., “Semidefinite Resolution and Exactness of Semidefinite Relaxations for Satisfiability”, Discrete Appl. Math., 161:18 (2013), 2812–2826  crossref  mathscinet  zmath  isi
    18. Atserias A., Lauria M., Nordstrom J., “Narrow Proofs May Be Maximally Long”, 2014 IEEE 29Th Conference on Computational Complexity (Ccc), IEEE Conference on Computational Complexity, IEEE, 2014, 286–297  crossref  mathscinet  isi
    19. Margulies S., Onn S., Pasechnik D.V., “on the Complexity of Hilbert Refutations For Partition”, J. Symbolic Comput., 66 (2015), 70–83  crossref  mathscinet  zmath  isi  elib
    20. Atserias A., Lauria M., Nordstrom J., “Narrow Proofs May Be Maximally Long”, ACM Trans. Comput. Log., 17:3 (2016), 19  crossref  mathscinet  zmath  isi
    21. Razborov A., “On the Width of Semialgebraic Proofs and Algorithms”, Math. Oper. Res., 42:4 (2017), 1106–1134  crossref  zmath  isi  scopus
  • Moscow Mathematical Journal
    Number of views:
    This page:135
    References:31

     
    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2019