Skip to main content
SpringerLink
Log in

Complexity of Semi-algebraic Proofs

  • Conference paper
  • First Online:
STACS 2002 (STACS 2002)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2285))

Included in the following conference series:

Abstract

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 LSd 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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Grigoriev, D., Hirsch, E.A., Pasechnik, D.V.: Complexity of semi-algebraic proofs. Technical report, Electronic Colloquim on Computational Complexity (2001(submitted)) http://eccc.uni-trier.de/eccc-local/Lists/TR-2001.html.

  2. Beame, P., Impagliazzo, R., Krajíček, J., Pitassi, T., Pudlák, P.: Lower bounds on Hilbert’s Nullstellensatz and propositional proofs. Proc. London Math. Soc. 73 (1996) 1–26

    Google Scholar 

  3. Beame, P., Impagliazzo, R., Krajíček, J., Pudlák, P., Razborov, A.A., Sgall, J.: Proof complexity in algebraic systems and bounded depth Frege systems with modular counting. Computational Complexity 6 (1996/97) 256–298

    Article  MathSciNet  Google Scholar 

  4. Razborov, A.A.: Lower bounds for the polynomial calculus. Computational Complexity 7 (1998) 291–324

    Article  MATH  MathSciNet  Google Scholar 

  5. Impagliazzo, R., Pudlák, P., Sgall, J.: Lower bounds for the polynomial calculus. Computational Complexity 8 (1999) 127–144

    Article  MATH  MathSciNet  Google Scholar 

  6. Clegg, M., Edmonds, J., Impagliazzo, R.: Using the Groebner basis algorithm to find proofs of unsatis.ability. In: Proceedings of the 28th Annual ACM Symposium on Theory of Computing, STOC’96, ACM (1996) 174–183

    Google Scholar 

  7. Buss, S., Grigoriev, D., Impagliazzo, R., Pitassi, T.: Linear gaps between degrees for the polynomial calculus modulo distinct primes. Journal of Computer and System Sciences 62 (2001) 267–289

    Article  MATH  MathSciNet  Google Scholar 

  8. Grigoriev, D., Hirsch, E.A.: Algebraic proof systems over formulas. Technical Report 01-011, Electronic Colloquim on Computational Complexity (2001) ftp://ftp.eccc.uni-trier.de/pub/eccc/reports/2001/TR01-011/index.html.

  9. Gomory, R.E.: An algorithm for integer solutions of linear programs. In: Recent Advances in Mathematical Programming. McGraw-Hill (1963) 269–302

    Google Scholar 

  10. Chvátal, V.: Edmonds polytopes and a hierarchy of combinatorial problems. Discrete Math. 4 (1973) 305–337

    Article  MATH  MathSciNet  Google Scholar 

  11. Cook, W., Coullard, C.R., Turán, G.: On the complexity of cutting-plane proofs. Discrete Appl. Math. 18(1987) 25–38

    Article  MATH  MathSciNet  Google Scholar 

  12. Chvátal, V., Cook, W., Hartmann, M.: On cutting-plane proofs in combinatorial optimization. Linear Algebra Appl. 114/115(1989) 455–499

    Article  MathSciNet  Google Scholar 

  13. Bonet, M., Pitassi, T., Raz, R.: Lower bounds for Cutting Planes proofs with small coeficients. In: Proceedings of the 27th Annual ACM Symposium on Theory of Computing, STOC’95, ACM (1995) 575–584

    Google Scholar 

  14. Pudlák, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic 62(1997) 981–998

    Article  MATH  MathSciNet  Google Scholar 

  15. Lovász, L., Schrijver, A.: Cones of matrices and set-functions and 0-1 optimization. SIAM Journal on Optimization 1 (1991) 166–190

    Article  MATH  MathSciNet  Google Scholar 

  16. Lovász, L.: Stable sets and polynomials. Discrete Mathematics 124 (1994) 137–153

    Article  MATH  MathSciNet  Google Scholar 

  17. Pudlák, P.: On the complexity of propositional calculus. In: Sets and Proofs: Invited papers from Logic Colloquium’97. Cambridge University Press (1999) 197–218

    Google Scholar 

  18. Razborov, A.: Lower bounds on the monotone complexity of boolean functions. Dokl. AN USSR 22(1985) 1033–1037

    Google Scholar 

  19. Grigoriev, D., Vorobjov, N.: Complexity of Null-and Positivstellensatz proofs. Annals of Pure and Applied Logic 113(2001) 153–160

    Article  MathSciNet  Google Scholar 

  20. Grigoriev, D.: Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity. Theoretical Computer Science 259 (2001) 613–622

    Google Scholar 

  21. Grigoriev, D.: Complexity of Positivstellensatz proofs for the knapsack. Computational Complexity 10(2001) 139–154

    Article  MATH  MathSciNet  Google Scholar 

  22. Stephen, T., Tunçel, L.: On a representation of the matching polytope via semidefinite liftings. Math. Oper. Res. 24 (1999) 1–7

    Article  MATH  MathSciNet  Google Scholar 

  23. Cook, W., Dash, S.: On the matrix-cut rank of polyhedra. Math. Oper. Res. 26 (2001) 19–30

    Article  MATH  MathSciNet  Google Scholar 

  24. Dash, S.: On the Matrix Cuts of Lovász and Schrijver and their use in Integer Programming. Technical report tr01-08, Rice University (2001) http://www.caam.rice.edu/caam/trs/2001/TR01-08.ps.

  25. Goemans, M.X., Tunçel, L.: When does the positive semidefiniteness constraint help in lifting procedures. Mathematics of Operations Research (2001) to appear.

    Google Scholar 

  26. Bockmayr, A., Eisenbrand, F., Hartmann, M., Schulz, A.S.: On the Chvátal rank of polytopes in the 0/1 cube. Discrete Applied Mathematics 98 (1999) 21–27

    Article  MATH  MathSciNet  Google Scholar 

  27. Eisenbrand, F., Schulz, A.S.: Bounds on the Chvátal rank of polytopes in the 0/1-cube. In G. Cornuéjos, R.E. Burkard, G., ed.: IPCO’99. Volume 1610 of Lecture Notes in Computer Science., Berlin Heidelberg, Springer-Verlag (1999) 137–150

    Google Scholar 

  28. Urquhart, A.: Hard examples for resolution. JACM 34 (1987)

    Google Scholar 

  29. Ben-Sasson, E.: Hard examples for bounded depth Frege. Manuscript (2001)

    Google Scholar 

  30. Krajíček, J.: Discretely ordered modules as a first-order extension of the cutting planes proof system. Journal of Symbolic Logic 63 (1998) 1582–1596

    Article  MATH  MathSciNet  Google Scholar 

  31. Cook, S.A., Reckhow, A.R.: The relative efficiency of propositional proof systems. Journal of Symbolic Logic 44 (1979) 36–50

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRMAR, Université de Rennes, Campus de Beaulieu, 35042, Rennes, cedex, France

    Dima Grigoriev

  2. Steklov Institute of Mathematics at St.Petersburg, 27 Fontanka, 191011, St.Petersburg, Russia

    Edward A. Hirsch

  3. Department of Technical Mathematics and Informatics, Faculty ITS, Delft, University of Technology, Mekelweg 4, 2628, CD Delft, The Netherlands

    Dmitrii V. Pasechnik

Authors
  1. Dima Grigoriev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Edward A. Hirsch
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Dmitrii V. Pasechnik
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Computer Science, Free University of Berlin, Takustraße 9, 14195, Berlin, Germany

    Helmut Alt

  2. CNRS - I3S - INRIA Sophia Antipolis, 2004 Route des Lucioles, 06902, Sophia Antipolis, France

    Afonso Ferreira

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Grigoriev, D., Hirsch, E.A., Pasechnik, D.V. (2002). Complexity of Semi-algebraic Proofs. In: Alt, H., Ferreira, A. (eds) STACS 2002. STACS 2002. Lecture Notes in Computer Science, vol 2285. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45841-7_34

Download citation

  • DOI: https://doi.org/10.1007/3-540-45841-7_34

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43283-8

  • Online ISBN: 978-3-540-45841-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation