Verifying Integer Programming Results

  • Kevin K. H. Cheung
  • Ambros Gleixner
  • Daniel E. SteffyEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10328)


Software for mixed-integer linear programming can return incorrect results for a number of reasons, one being the use of inexact floating-point arithmetic. Even solvers that employ exact arithmetic may suffer from programming or algorithmic errors, motivating the desire for a way to produce independently verifiable certificates of claimed results. Due to the complex nature of state-of-the-art MIP solution algorithms, the ideal form of such a certificate is not entirely clear. This paper proposes such a certificate format designed with simplicity in mind, which is composed of a list of statements that can be sequentially verified using a limited number of inference rules. We present a supplementary verification tool for compressing and checking these certificates independently of how they were created. We report computational results on a selection of MIP instances from the literature. To this end, we have extended the exact rational version of the MIP solver SCIP to produce such certificates.


Correctness Verification Proof Certificate Optimality Infeasibility Mixed-integer linear programming 



We thank Kati Wolter for the exact version of SCIP [13] and Daniel Espinoza for QSopt_ex [7], which provided the basis for our experiments, and Gregor Hendel for his Ipet package [26], which was a big help in analyzing the experimental results. This work has been supported by the Research Campus MODAL Mathematical Optimization and Data Analysis Laboratories funded by the Federal Ministry of Education and Research (BMBF Grant 05M14ZAM). All responsibility for the content of this publication is assumed by the authors.


  1. 1.
    Achterberg, T.: Constraint Integer Programming. Ph.D. Thesis, TU Berlin (2007)Google Scholar
  2. 2.
    Achterberg, T., Koch, T., Martin, A.: The mixed integer programming library: MIPLIB 2003. Oper. Res. Lett. 34(4), 361–372 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Achterberg, T., Wunderling, R.: Mixed integer programming: analyzing 12 years of progress. In: Jünger, M., Reinelt, G. (eds.) Facets of Combinatorial Optimization: Festschrift for Martin Grötschel, pp. 449–481. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  4. 4.
    Bixby, R.E., Fenelon, M., Gu, Z., Rothberg, E., Wunderling, R.: MIP: theory and practice - closing the gap. In: Powell, M.J.D., Scholtes, S. (eds.) System Modelling and Optimization, pp. 19–49 (2000)Google Scholar
  5. 5.
    Applegate, D.L., Bixby, R.E., Chvátal, V., Cook, W., Espinoza, D.G., Goycoolea, M., Helsgaun, K.: Certification of an optimal TSP tour through 85,900 cities. Oper. Res. Lett. 37, 11–15 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Applegate, D.L., Cook, W.J., Dash, S., Espinoza, D.G.: Exact solutions to linear programming problems. Oper. Res. Lett. 35(6), 693–699 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Applegate, D.L., Cook, W.J., Dash, S., Espinoza, D.G.: QSopt_ex: bico/qsopt/ex/. Last accessed 13 Nov 2016
  8. 8.
    Balas, E., Fischetti, M., Zanette, A.: A hard integer program made easy by lexicography. Math. Program. Ser. A 135, 509–514 (2012)CrossRefzbMATHGoogle Scholar
  9. 9.
    Bixby, R.E., Ceria, S., McZeal, C.M., Savelsbergh, M.W.: An updated mixed integer programming library: MIPLIB 3.0. Optima 58, 12–15 (1998)Google Scholar
  10. 10.
    Boland, N.L., Eberhard, A.C.: On the augmented Lagrangian dual for integer programming. Math. Program. Ser. A 150(2), 491–509 (2015)MathSciNetCrossRefzbMATHGoogle Scholar
  11. 11.
    Carr, R., Greenberg, H., Parekh, O., Phillips, C.: Towards certificates for integer programming computations. Presentation, 2011 DOE Applied Mathematics PI meeting, October 2011. Slides Last accessed 13 Nov 2016
  12. 12.
    Cook, W., Dash, S., Fukasawa, R., Goycoolea, M.: Numerically safe Gomory mixed-integer cuts. INFORMS J. Comput. 21(4), 641–649 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Cook, W., Koch, T., Steffy, D., Wolter, K.: A hybrid branch-and-bound approach for exact rational mixed-integer programming. Math. Program. Comput. 3, 305–344 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Cornuéjols, G.: Valid inequalities for mixed integer linear programs. Math. Program. Ser. B 112, 3–44 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Cornuéjols, G., Liberti, L., Nannicini, G.: Improved strategies for branching on general disjunctions. Math. Program. Ser. A 130, 225–247 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    De Loera, J.A., Lee, J., Malkin, P.N., Margulies, S.: Computing infeasibility certificates for combinatorial problems through Hilberts Nullstellensatz. J. Symbolic Comp. 46(11), 1260–1283 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Dhiflaoui, M., Funke, S., Kwappik, C., Mehlhorn, K., Seel, M., Schomer, E., Schulte, R., Weber, D.: Certifying and repairing solutions to large LPs, how good are LP-solvers? In: SODA 2003, pp. 255–256. ACM/SIAM, New York (2003)Google Scholar
  18. 18.
    Fukasawa, R., Goycoolea, M.: On the exact separation of mixed integer knapsack cuts. Math. Program. Ser. A 128, 19–41 (2008)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    The Flyspeck Project. Last accessed 13 Nov 2016
  20. 20.
    Gamrath, G., Melchiori, A., Berthold, T., Gleixner, A.M., Salvagnin, D.: Branching on multi-aggregated variables. In: Michel, L. (ed.) CPAIOR 2015. LNCS, vol. 9075, pp. 141–156. Springer, Cham (2015). doi: 10.1007/978-3-319-18008-3_10 Google Scholar
  21. 21.
    Gamrath, G., et al.: The SCIP Optimization Suite 3.2. ZIB-Report (15–60) (2016)Google Scholar
  22. 22.
    GNU MP: The GNU Multiple Precision Arithmetic Library version 6.1.1. Last accessed 16 Nov 2016
  23. 23.
    Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bull. Amer. Math. Soc. 64, 275–278 (1958)MathSciNetCrossRefzbMATHGoogle Scholar
  24. 24.
    Guzelsoy, M., Ralphs, T.K.: Duality for mixed-integer linear programs. Int. J. Oper. Res. 4(3), 118–137 (2007)MathSciNetzbMATHGoogle Scholar
  25. 25.
    Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996). doi: 10.1007/BFb0031814 CrossRefGoogle Scholar
  26. 26.
    Hendel, G.: Empirical analysis of solving phases in mixed integer programming. Master’s thesis, Technische Universität Berlin (2014). urn:nbn:de:0297-zib-54270
  27. 27.
    Heule, M.J.H., Hunt, W.A., Wetzler, N.: Verifying refutations with extended resolution. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 345–359. Springer, Heidelberg (2013). doi: 10.1007/978-3-642-38574-2_24 CrossRefGoogle Scholar
  28. 28.
    Hooker, J.N.: Integrated Methods for Optimization, 2nd edn. Springer, New York (2012)CrossRefzbMATHGoogle Scholar
  29. 29.
  30. 30.
    Karamanov, M., Cornuéjols, G.: Branching on general disjunctions. Math. Program. Ser. A 128, 403–436 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Klabjan, D.: Subadditive approaches in integer programming. Eur. J. Oper. Res. 183, 525–545 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  32. 32.
    Koch, T., Achterberg, T., Andersen, E., Bastert, O., Berthold, T., Bixby, R.E., Danna, E., Gamrath, G., Gleixner, A.M., Heinz, S., Lodi, A., Mittelmann, H., Ralphs, T., Salvagnin, D., Steffy, D.E., Wolter, K.: MIPLIB 2010. Math. Program. Comp. 3(2), 103–163 (2011)CrossRefGoogle Scholar
  33. 33.
    Lasserre, J.B.: Generating functions and duality for integer programs. Discrete Optim. 1(2), 167–187 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    Lehigh University COR@L mixed integer programming collection. Last accessed 18 Nov 2016
  35. 35.
    Mittelmann, H.D.: Benchmarks for Optimization Software. Last accessed 18 Nov 2016
  36. 36.
    Narkawicz, A., Muñoz, C.: A formally verified generic branching algorithm for global optimization. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 326–343. Springer, Heidelberg (2014). doi: 10.1007/978-3-642-54108-7_17 CrossRefGoogle Scholar
  37. 37.
    Neumaier, A., Shcherbina, O.: Safe bounds in linear and mixed-integer linear programming. Math. Program. 99(2), 283–296 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  38. 38.
    Owen, J.H., Mehrotra, S.: Experimental results on using general disjunctions in branch-and-bound for general-integer linear programs. Comput. Optim. Appl. 20, 159–170 (2001)MathSciNetCrossRefzbMATHGoogle Scholar
  39. 39.
    Obua, S., Nipkow, T.: Flyspeck II: the basic linear programs. Ann. Math. Artif. Intell 56, 245–272 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  40. 40.
    Pulaj, J.: Cutting Planes for Families Implying Frankl’s Conjecture. ZIB-Report (16–51) (2016). urn:nbn:de:0297-zib-60626
  41. 41.
    Smith, A.P., Muñoz, C.A., Narkawicz, A.J., Markevicius, M.: Kodiak: an Implementation Framework for Branch and Bound Algorithms. Technical report: NASA/TM-2015-218776 (2015)Google Scholar
  42. 42.
    Solovyev, A., Hales, T.C.: Efficient formal verification of bounds of linear programs. In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS, vol. 6824, pp. 123–132. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22673-1_9 CrossRefGoogle Scholar
  43. 43.
    Wetzler, N., Heule, M.J.H., Hunt, W.A.: DRAT-trim: efficient checking and trimming using expressive clausal proofs. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 422–429. Springer, Cham (2014). doi: 10.1007/978-3-319-09284-3_31 Google Scholar
  44. 44.
    Zanette, A., Fischetti, M., Balas, E.: Lexicography and degeneracy: can a pure cutting plane algorithm work? Math. Program. Ser. A 130, 153–176 (2011)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Kevin K. H. Cheung
    • 1
  • Ambros Gleixner
    • 2
  • Daniel E. Steffy
    • 3
    Email author
  1. 1.School of Mathematics and StatisticsCarleton UniversityOttawaCanada
  2. 2.Department of Mathematical OptimizationZuse Institute BerlinBerlinGermany
  3. 3.Department of Mathematics and StatisticsOakland UniversityRochesterUSA

Personalised recommendations