{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T13:12:19Z","timestamp":1776863539630,"version":"3.51.2"},"publisher-location":"Cham","reference-count":44,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319592497","type":"print"},{"value":"9783319592503","type":"electronic"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-59250-3_13","type":"book-chapter","created":{"date-parts":[[2017,5,23]],"date-time":"2017-05-23T13:04:39Z","timestamp":1495544679000},"page":"148-160","source":"Crossref","is-referenced-by-count":20,"title":["Verifying Integer Programming Results"],"prefix":"10.1007","author":[{"given":"Kevin K. H.","family":"Cheung","sequence":"first","affiliation":[]},{"given":"Ambros","family":"Gleixner","sequence":"additional","affiliation":[]},{"given":"Daniel E.","family":"Steffy","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,5,24]]},"reference":[{"key":"13_CR1","unstructured":"Achterberg, T.: Constraint Integer Programming. Ph.D. Thesis, TU Berlin (2007)"},{"issue":"4","key":"13_CR2","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1016\/j.orl.2005.07.009","volume":"34","author":"T Achterberg","year":"2006","unstructured":"Achterberg, T., Koch, T., Martin, A.: The mixed integer programming library: MIPLIB 2003. Oper. Res. Lett. 34(4), 361\u2013372 (2006)","journal-title":"Oper. Res. Lett."},{"key":"13_CR3","doi-asserted-by":"crossref","first-page":"449","DOI":"10.1007\/978-3-642-38189-8_18","volume-title":"Facets of Combinatorial Optimization: Festschrift for Martin Gr\u00f6tschel","author":"T Achterberg","year":"2013","unstructured":"Achterberg, T., Wunderling, R.: Mixed integer programming: analyzing 12 years of progress. In: J\u00fcnger, M., Reinelt, G. (eds.) Facets of Combinatorial Optimization: Festschrift for Martin Gr\u00f6tschel, pp. 449\u2013481. Springer, Heidelberg (2013)"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"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\u201349 (2000)","DOI":"10.1007\/978-0-387-35514-6_2"},{"key":"13_CR5","doi-asserted-by":"crossref","first-page":"11","DOI":"10.1016\/j.orl.2008.09.006","volume":"37","author":"DL Applegate","year":"2009","unstructured":"Applegate, D.L., Bixby, R.E., Chv\u00e1tal, 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\u201315 (2009)","journal-title":"Oper. Res. Lett."},{"issue":"6","key":"13_CR6","doi-asserted-by":"crossref","first-page":"693","DOI":"10.1016\/j.orl.2006.12.010","volume":"35","author":"DL Applegate","year":"2007","unstructured":"Applegate, D.L., Cook, W.J., Dash, S., Espinoza, D.G.: Exact solutions to linear programming problems. Oper. Res. Lett. 35(6), 693\u2013699 (2007)","journal-title":"Oper. Res. Lett."},{"key":"13_CR7","unstructured":"Applegate, D.L., Cook, W.J., Dash, S., Espinoza, D.G.: QSopt_ex: \nhttp:\/\/www.math.uwaterloo.ca\/ bico\/qsopt\/ex\/\n\n. Last accessed 13 Nov 2016"},{"key":"13_CR8","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1007\/s10107-011-0450-6","volume":"135","author":"E Balas","year":"2012","unstructured":"Balas, E., Fischetti, M., Zanette, A.: A hard integer program made easy by lexicography. Math. Program. Ser. A 135, 509\u2013514 (2012)","journal-title":"Math. Program. Ser. A"},{"key":"13_CR9","first-page":"12","volume":"58","author":"RE Bixby","year":"1998","unstructured":"Bixby, R.E., Ceria, S., McZeal, C.M., Savelsbergh, M.W.: An updated mixed integer programming library: MIPLIB 3.0. Optima 58, 12\u201315 (1998)","journal-title":"Optima"},{"issue":"2","key":"13_CR10","doi-asserted-by":"crossref","first-page":"491","DOI":"10.1007\/s10107-014-0763-3","volume":"150","author":"NL Boland","year":"2015","unstructured":"Boland, N.L., Eberhard, A.C.: On the augmented Lagrangian dual for integer programming. Math. Program. Ser. A 150(2), 491\u2013509 (2015)","journal-title":"Math. Program. Ser. A"},{"key":"13_CR11","unstructured":"Carr, R., Greenberg, H., Parekh, O., Phillips, C.: Towards certificates for integer programming computations. Presentation, 2011 DOE Applied Mathematics PI meeting, October 2011. Slides \nwww.csm.ornl.gov\/workshops\/applmath11\/documents\/talks\/Phillips_talk.pdf\n\n. Last accessed 13 Nov 2016"},{"issue":"4","key":"13_CR12","doi-asserted-by":"crossref","first-page":"641","DOI":"10.1287\/ijoc.1090.0324","volume":"21","author":"W Cook","year":"2009","unstructured":"Cook, W., Dash, S., Fukasawa, R., Goycoolea, M.: Numerically safe Gomory mixed-integer cuts. INFORMS J. Comput. 21(4), 641\u2013649 (2009)","journal-title":"INFORMS J. Comput."},{"key":"13_CR13","doi-asserted-by":"crossref","first-page":"305","DOI":"10.1007\/s12532-013-0055-6","volume":"3","author":"W Cook","year":"2013","unstructured":"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\u2013344 (2013)","journal-title":"Math. Program. Comput."},{"key":"13_CR14","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10107-006-0086-0","volume":"112","author":"G Cornu\u00e9jols","year":"2008","unstructured":"Cornu\u00e9jols, G.: Valid inequalities for mixed integer linear programs. Math. Program. Ser. B 112, 3\u201344 (2008)","journal-title":"Math. Program. Ser. B"},{"key":"13_CR15","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1007\/s10107-009-0333-2","volume":"130","author":"G Cornu\u00e9jols","year":"2011","unstructured":"Cornu\u00e9jols, G., Liberti, L., Nannicini, G.: Improved strategies for branching on general disjunctions. Math. Program. Ser. A 130, 225\u2013247 (2011)","journal-title":"Math. Program. Ser. A"},{"issue":"11","key":"13_CR16","doi-asserted-by":"crossref","first-page":"1260","DOI":"10.1016\/j.jsc.2011.08.007","volume":"46","author":"JA Loera De","year":"2011","unstructured":"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\u20131283 (2011)","journal-title":"J. Symbolic Comp."},{"key":"13_CR17","unstructured":"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\u2013256. ACM\/SIAM, New York (2003)"},{"key":"13_CR18","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1007\/s10107-009-0284-7","volume":"128","author":"R Fukasawa","year":"2008","unstructured":"Fukasawa, R., Goycoolea, M.: On the exact separation of mixed integer knapsack cuts. Math. Program. Ser. A 128, 19\u201341 (2008)","journal-title":"Math. Program. Ser. A"},{"key":"13_CR19","unstructured":"The Flyspeck Project. \nhttps:\/\/code.google.com\/archive\/p\/flyspeck\/\n\n. Last accessed 13 Nov 2016"},{"key":"13_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-319-18008-3_10","volume-title":"Integration of AI and OR Techniques in Constraint Programming","author":"G Gamrath","year":"2015","unstructured":"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\u2013156. Springer, Cham (2015). doi:\n10.1007\/978-3-319-18008-3_10"},{"key":"13_CR21","unstructured":"Gamrath, G., et al.: The SCIP Optimization Suite 3.2. ZIB-Report (15\u201360) (2016)"},{"key":"13_CR22","unstructured":"GNU MP: The GNU Multiple Precision Arithmetic Library version 6.1.1. \nhttp:\/\/gmplib.org\n\n. Last accessed 16 Nov 2016"},{"key":"13_CR23","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1090\/S0002-9904-1958-10224-4","volume":"64","author":"RE Gomory","year":"1958","unstructured":"Gomory, R.E.: Outline of an algorithm for integer solutions to linear programs. Bull. Amer. Math. Soc. 64, 275\u2013278 (1958)","journal-title":"Bull. Amer. Math. Soc."},{"issue":"3","key":"13_CR24","first-page":"118","volume":"4","author":"M Guzelsoy","year":"2007","unstructured":"Guzelsoy, M., Ralphs, T.K.: Duality for mixed-integer linear programs. Int. J. Oper. Res. 4(3), 118\u2013137 (2007)","journal-title":"Int. J. Oper. Res."},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265\u2013269. Springer, Heidelberg (1996). doi:\n10.1007\/BFb0031814"},{"key":"13_CR26","unstructured":"Hendel, G.: Empirical analysis of solving phases in mixed integer programming. Master\u2019s thesis, Technische Universit\u00e4t Berlin (2014). \nurn:nbn:de:0297-zib-54270"},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-642-38574-2_24","volume-title":"Automated Deduction \u2013 CADE-24","author":"MJH Heule","year":"2013","unstructured":"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\u2013359. Springer, Heidelberg (2013). doi:\n10.1007\/978-3-642-38574-2_24"},{"key":"13_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4614-1900-6","volume-title":"Integrated Methods for Optimization","author":"JN Hooker","year":"2012","unstructured":"Hooker, J.N.: Integrated Methods for Optimization, 2nd edn. Springer, New York (2012)","edition":"2"},{"key":"13_CR29","unstructured":"IBM ILOG. CPLEX. \nhttps:\/\/www-01.ibm.com\/software\/commerce\/optimization\/cplex-optimizer\/\n\n. Last accessed 16 Nov 2016"},{"key":"13_CR30","doi-asserted-by":"crossref","first-page":"403","DOI":"10.1007\/s10107-009-0332-3","volume":"128","author":"M Karamanov","year":"2011","unstructured":"Karamanov, M., Cornu\u00e9jols, G.: Branching on general disjunctions. Math. Program. Ser. A 128, 403\u2013436 (2011)","journal-title":"Math. Program. Ser. A"},{"key":"13_CR31","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1016\/j.ejor.2006.10.009","volume":"183","author":"D Klabjan","year":"2007","unstructured":"Klabjan, D.: Subadditive approaches in integer programming. Eur. J. Oper. Res. 183, 525\u2013545 (2007)","journal-title":"Eur. J. Oper. Res."},{"issue":"2","key":"13_CR32","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/s12532-011-0025-9","volume":"3","author":"T Koch","year":"2011","unstructured":"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\u2013163 (2011)","journal-title":"Math. Program. Comp."},{"issue":"2","key":"13_CR33","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/j.disopt.2003.12.002","volume":"1","author":"JB Lasserre","year":"2004","unstructured":"Lasserre, J.B.: Generating functions and duality for integer programs. Discrete Optim. 1(2), 167\u2013187 (2004)","journal-title":"Discrete Optim."},{"key":"13_CR34","unstructured":"Lehigh University COR@L mixed integer programming collection. \nhttp:\/\/coral.ie.lehigh.edu\/wiki\/doku.php\/info:datasets:mip\n\n. Last accessed 18 Nov 2016"},{"key":"13_CR35","unstructured":"Mittelmann, H.D.: Benchmarks for Optimization Software. \nhttp:\/\/plato.asu.edu\/bench.html\n\n Last accessed 18 Nov 2016"},{"key":"13_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-54108-7_17","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A Narkawicz","year":"2014","unstructured":"Narkawicz, A., Mu\u00f1oz, C.: A formally verified generic branching algorithm for global optimization. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 326\u2013343. Springer, Heidelberg (2014). doi:\n10.1007\/978-3-642-54108-7_17"},{"issue":"2","key":"13_CR37","doi-asserted-by":"crossref","first-page":"283","DOI":"10.1007\/s10107-003-0433-3","volume":"99","author":"A Neumaier","year":"2004","unstructured":"Neumaier, A., Shcherbina, O.: Safe bounds in linear and mixed-integer linear programming. Math. Program. 99(2), 283\u2013296 (2004)","journal-title":"Math. Program."},{"key":"13_CR38","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1023\/A:1011207119557","volume":"20","author":"JH Owen","year":"2001","unstructured":"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\u2013170 (2001)","journal-title":"Comput. Optim. Appl."},{"key":"13_CR39","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1007\/s10472-009-9168-z","volume":"56","author":"S Obua","year":"2009","unstructured":"Obua, S., Nipkow, T.: Flyspeck II: the basic linear programs. Ann. Math. Artif. Intell 56, 245\u2013272 (2009)","journal-title":"Ann. Math. Artif. Intell"},{"key":"13_CR40","unstructured":"Pulaj, J.: Cutting Planes for Families Implying Frankl\u2019s Conjecture. ZIB-Report (16\u201351) (2016). \nurn:nbn:de:0297-zib-60626"},{"key":"13_CR41","unstructured":"Smith, A.P., Mu\u00f1oz, C.A., Narkawicz, A.J., Markevicius, M.: Kodiak: an Implementation Framework for Branch and Bound Algorithms. Technical report: NASA\/TM-2015-218776 (2015)"},{"key":"13_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-22673-1_9","volume-title":"Intelligent Computer Mathematics","author":"A Solovyev","year":"2011","unstructured":"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\u2013132. Springer, Heidelberg (2011). doi:\n10.1007\/978-3-642-22673-1_9"},{"key":"13_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1007\/978-3-319-09284-3_31","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"N Wetzler","year":"2014","unstructured":"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\u2013429. Springer, Cham (2014). doi:\n10.1007\/978-3-319-09284-3_31"},{"key":"13_CR44","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/s10107-009-0335-0","volume":"130","author":"A Zanette","year":"2011","unstructured":"Zanette, A., Fischetti, M., Balas, E.: Lexicography and degeneracy: can a pure cutting plane algorithm work? Math. Program. Ser. A 130, 153\u2013176 (2011)","journal-title":"Math. Program. Ser. A"}],"container-title":["Lecture Notes in Computer Science","Integer Programming and Combinatorial Optimization"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-59250-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,5,23]],"date-time":"2017-05-23T13:07:39Z","timestamp":1495544859000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-59250-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319592497","9783319592503"],"references-count":44,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-59250-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017]]}}}