Skip to main content
SpringerLink
Log in

Toward Computer-Assisted Discovery and Automated Proofs of Cutting Plane Theorems

  • Conference paper
  • First Online:
Combinatorial Optimization (ISCO 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9849))

Included in the following conference series:

Abstract

Using a metaprogramming technique and semialgebraic computations, we provide computer-based proofs for old and new cutting-plane theorems in Gomory–Johnson’s model of cut generating functions.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Notes

  1. 1.

    A function name shown in typewriter font is the name of the constructor of this function in the Electronic Compendium, part of the SageMath program [20]. In an online copy of this paper, hyperlinks lead to this function in the GitHub repository.

  2. 2.

    This is a new result, which should not be confused with our previous result in [22] regarding Chen’s family of 3-slope functions (chen_3_slope_not_extreme, ).

  3. 3.

    The finiteness proof of the algorithm, however, does depend on the rationality of the data. In this paper we shall ignore the case of functions with non-covered intervals and irrational breakpoints, such as the bhk_irrational (https://github.com/mkoeppe/infinite-group-relaxation-code/search?q=%22def+bhk_irrational(%22) family.

  4. 4.

    These elements are instances of the class ParametricRealFieldElement. Their parent, representing the field, is an instance of the class ParametricRealField.

  5. 5.

    Since all expressions are, in fact, rational functions, we use exact seminumerical computations in the quotient field of a multivariate polynomial ring, instead of the slower and less robust general symbolic computation facility.

  6. 6.

    This information is recorded in the parent of the elements.

  7. 7.

    We plan to automate this in a future version of our software.

References

  1. Appel, K., Haken, W.: Every planar map is four colorable. Part I: discharging. Illinois J. Math. 21(3), 429–490 (1977). http://projecteuclid.org/euclid.ijm/1256049011

    MathSciNet  MATH  Google Scholar 

  2. Bagnara, R., Hill, P.M., Zaffanella, E.: The Parma Polyhedra Library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1–2), 3–21 (2008). http://dx.doi.org/dx.doi.org/10.1016/j.scico.2007.08.001

    Article  MathSciNet  Google Scholar 

  3. Basu, A., Hildebrand, R., Köppe, M.: Equivariant perturbation in Gomory and Johnson’s infinite group problem. I. The one-dimensional case. Math. Oper. Res. 40(1), 105–129 (2014). doi:10.1287/moor.2014.0660

    Article  MATH  Google Scholar 

  4. Basu, A., Hildebrand, R., Köppe, M.: Light on the infinite group relaxation I: foundations and taxonomy. 4OR 14(1), 1–40 (2016). doi:10.1007/s10288-015-0292-9

    Article  MathSciNet  MATH  Google Scholar 

  5. Basu, A., Hildebrand, R., Köppe, M.: Light on the infinite group relaxation II: sufficient conditions for extremality, sequences, and algorithms. 4OR 14(2), 107–131 (2016). doi:10.1007/s10288-015-0293-8

    Article  MathSciNet  MATH  Google Scholar 

  6. Basu, S., Pollack, R., Roy, M.-F.: Algorithms in Real Algebraic Geometry. Algorithms and Computation in Mathematics, vol. 10. Springer, Berlin (2006). MR2248869 (2007b:14125), ISBN:978-3-540-33098-1; 3–540-33098-4

    MATH  Google Scholar 

  7. Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. SIGSAM Bull. 37(4), 97–108 (2003). doi:10.1145/968708.968710

    Article  MATH  Google Scholar 

  8. Chen, K.: Topics in group methods for integer programming. Ph.D. thesis, Georgia Institute of Technology, June 2011

    Google Scholar 

  9. Christof, T., Löbel, A.: Porta: Polyhedron representation transformation algorithm. http://comopt.ifi.uni-heidelberg.de/software/PORTA/

  10. Conforti, M., Cornuéjols, G., Daniilidis, A., Lemaréchal, C., Malick, J.: Cut-generating functions and S-free sets. Math. Oper. Res. 40(2), 253–275 (2013). http://dx.doi.org/10.1287/moor.2014.0670

    MathSciNet  MATH  Google Scholar 

  11. Conforti, M., Cornuéjols, G., Zambelli, G.: Corner polyhedra and intersection cuts. Surv. Oper. Res. Manag. Sci. 16, 105–120 (2011)

    MATH  Google Scholar 

  12. Dey, S.S., Richard, J.-P.P., Li, Y., Miller, L.A.: On the extreme inequalities of infinite group problems. Math. Program. 121(1), 145–170 (2010). doi:10.1007/s10107-008-0229-6

    Article  MathSciNet  MATH  Google Scholar 

  13. Ekhad XIV, S.B., Zeilberger, D.: Plane geometry: an elementary textbook, 2050. http://www.math.rutgers.edu/~zeilberg/GT.html

  14. Gomory, R.E., Johnson, E.L.: Some continuous functions related to corner polyhedra, I. Math. Program. 3, 23–85 (1972). doi:10.1007/BF01584976

    Article  MathSciNet  MATH  Google Scholar 

  15. Gomory, R.E., Johnson, E.L.: Some continuous functions related to corner polyhedra, II. Math. Program. 3, 359–389 (1972). doi:10.1007/BF01585008

    Article  MathSciNet  MATH  Google Scholar 

  16. Gomory, R.E., Johnson, E.L.: T-space and cutting planes. Math. Program. 96, 341–375 (2003). doi:10.1007/s10107-003-0389-3

    Article  MathSciNet  MATH  Google Scholar 

  17. Goodman, J.E., O’Rourke, J. (eds.): Handbook of Discrete and Computational Geometry. CRC Press Inc., Boca Raton (1997). ISBN:0-8493-8524-5

    MATH  Google Scholar 

  18. Hales, T.C.: A proof of the Kepler conjecture. Ann. of Math. 162(3), 1065–1185 (2005). doi:10.4007/annals.2005.162.1065. MR2179728 (2006g:52029)

    Article  MathSciNet  MATH  Google Scholar 

  19. Hales, T.C., Adams, M., Bauer, G., Dang, D.T., Harrison, J., Hoang, T.L., Kaliszyk, C., Magron, V., McLaughlin, S., Nguyen, T.T., et al.: A formal proof of the Kepler conjecture (2015). arXiv preprint arXiv:1501.02155

  20. Hong, C.Y., Köppe, M., Zhou, Y.: SageMath program for computation and experimentation with the \(1\)-dimensional Gomory-Johnson infinite group problem (2014). http://github.com/mkoeppe/infinite-group-relaxation-code

  21. Johnson, E.L.: On the group problem for mixed integer programming. Math. Program. Study 2, 137–179 (1974)

    Article  MathSciNet  Google Scholar 

  22. Köppe, M., Zhou, Y.: An electronic compendium of extreme functions for the Gomory-Johnson infinite group problem. Oper. Res. Lett. 43(4), 438–444 (2015). doi:10.1016/j.orl.2015.06.004

    Article  MathSciNet  Google Scholar 

  23. Köppe, M., Zhou, Y.: New computer-based search strategies for extreme functions of the Gomory-Johnson infinite group problem (2015). arXiv:1506.00017 [math.OC]

  24. Miller, L.A., Li, Y., Richard, J.-P.P.: New inequalities for finite and infinite group problems from approximate lifting. Naval Res. Logist. (NRL) 55(2), 172–191 (2008). doi:10.1002/nav.20275

    Article  MathSciNet  MATH  Google Scholar 

  25. Richard, J.-P.P., Li, Y., Miller, L.A.: Valid inequalities for MIPs and group polyhedra from approximate liftings. Math. Program. 118(2), 253–277 (2009). doi:10.1007/s10107-007-0190-9

    Article  MathSciNet  MATH  Google Scholar 

  26. Stein, W.A., et al.: Sage Mathematics Software (Version 7.1). The Sage Development Team (2016). http://www.sagemath.org

  27. Sugiyama, M.: Cut-generating functions for integer linear programming. Bachelor thesis, UC Davis, June 2015. https://www.math.ucdavis.edu/files/1514/4469/2452/Masumi_Sugiyama_ugrad_thesis.pdf

  28. Wiedijk, F.: The seventeen provers of the world. http://www.cs.ru.nl/~freek/comparison/comparison.pdf

Download references

Author information

Authors and Affiliations

  1. Department of Mathematics, University of California, Davis, CA, USA

    Matthias Köppe & Yuan Zhou

Authors
  1. Matthias Köppe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Yuan Zhou
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Matthias Köppe .

Editor information

Editors and Affiliations

  1. University of Salerno , Fisciano, Italy

    Raffaele Cerulli

  2. Kyoto University , Kyoto, Japan

    Satoru Fujishige

  3. LAMSADE, Université Paris-Dauphine , Paris , France

    A. Ridha Mahjoub

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Köppe, M., Zhou, Y. (2016). Toward Computer-Assisted Discovery and Automated Proofs of Cutting Plane Theorems. In: Cerulli, R., Fujishige, S., Mahjoub, A. (eds) Combinatorial Optimization. ISCO 2016. Lecture Notes in Computer Science(), vol 9849. Springer, Cham. https://doi.org/10.1007/978-3-319-45587-7_29

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-45587-7_29

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-45586-0

  • Online ISBN: 978-3-319-45587-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation