Document Open Access Logo

VIPR Certificate Construction from Black-Box ILP Solvers

Author Stefan Szeider

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2026.52.pdf
  • Filesize: 0.89 MB
  • 14 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorial optimization
  • Theory of computation → Integer programming
Keywords
  • Integer linear programming
  • VIPR certificates
  • LP duality
  • branch and bound
  • solver verification

Metrics

Abstract

We propose an oracle-guided approach to construct VIPR certificates that certify the optimality of integer linear programming (ILP) solutions. Our approach treats the ILP solver as a black-box oracle and translates its floating-point answers into exact rational derivations. This translation is based on the notion of cascaded rationalization, a sequence of continued-fraction approximations at increasing precision levels. Our approach does not require an exact LP solver and comes with self-contained, independently verifiable VIPR certificates. We implement this approach and evaluate it empirically against Scip’s exact mode on generated benchmarks across four problem classes and on MIPLIB 2017 instances. On generated benchmarks, the oracle approach produces substantially more compact certificates on nearly all instances. On MIPLIB, each approach solves instances that the other cannot handle. The two approaches to certified optimality are complementary.

Cite As Get BibTex

Stefan Szeider. VIPR Certificate Construction from Black-Box ILP Solvers. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 52:1-52:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CP.2026.52

Author Details

Stefan Szeider
  • TU Wien, Vienna, Austria

Funding

Supported by the Austrian Science Fund (FWF), projects 10.55776/COE12 and 10.55776/P36420.

Supplementary Materials

References

  1. David L. Applegate, Robert E. Bixby, Vasek Chvátal, and William J. Cook. The Traveling Salesman Problem: A Computational Study. Princeton University Press, 2006. Google Scholar
  2. Sander Borst, Leon Eifler, and Ambros Gleixner. Certified constraint propagation and dual proof analysis in a numerically exact MIP solver, 2024. URL: https://arxiv.org/abs/2403.13567.
  3. Kevin K. H. Cheung, Ambros M. Gleixner, and Daniel E. Steffy. Verifying integer programming results. In Friedrich Eisenbrand and Jochen Könemann, editors, Integer Programming and Combinatorial Optimization - 19th International Conference, IPCO 2017, Waterloo, ON, Canada, June 26-28, 2017, Proceedings, Lecture Notes in Computer Science, pages 148-160. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-59250-3_13.
  4. William J. Cook, Thorsten Koch, Daniel E. Steffy, and Kati Wolter. A hybrid branch-and-bound approach for exact rational mixed-integer programming. Math. Program. Comput., 5(3):305-344, 2013. URL: https://doi.org/10.1007/S12532-013-0055-6.
  5. Leon Eifler and Ambros M. Gleixner. A computational status update for exact rational mixed integer programming. Math. Program., 197(2):793-812, 2023. URL: https://doi.org/10.1007/S10107-021-01749-5.
  6. Leon Eifler and Ambros M. Gleixner. Safe and verified gomory mixed-integer cuts in a rational mixed-integer program framework. SIAM J. Optim., 34(1):742-763, 2024. URL: https://doi.org/10.1137/23M156046X.
  7. Jan Elffers, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Justifying all differences using pseudo-boolean reasoning. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, pages 1486-1494. AAAI Press, 2020. URL: https://doi.org/10.1609/AAAI.V34I02.5507.
  8. Ambros M. Gleixner, Gregor Hendel, Gerald Gamrath, Tobias Achterberg, Michael Bastubbe, Timo Berthold, Philipp M. Christophel, Kati Jarck, Thorsten Koch, Jeff T. Linderoth, Marco E. Lübbecke, Hans D. Mittelmann, Derya B. Özyurt, Ted K. Ralphs, Domenico Salvagnin, and Yuji Shinano. MIPLIB 2017: data-driven compilation of the 6th mixed-integer programming library. Math. Program. Comput., 13(3):443-490, 2021. URL: https://doi.org/10.1007/S12532-020-00194-3.
  9. Ambros M. Gleixner and Daniel E. Steffy. Linear programming using limited-precision oracles. Math. Program., 183(1):525-554, 2020. URL: https://doi.org/10.1007/S10107-019-01444-6.
  10. Ambros M. Gleixner, Daniel E. Steffy, and Kati Wolter. Iterative refinement for linear programming. INFORMS J. Comput., 28(3):449-464, 2016. URL: https://doi.org/10.1287/IJOC.2016.0692.
  11. Alexander Hoen and Ambros M. Gleixner. Analyzing the numerical correctness of branch-and-bound decisions for mixed-integer programming. In Guido Tack, editor, Integration of Constraint Programming, Artificial Intelligence, and Operations Research - 22nd International Conference, CPAIOR 2025, Melbourne, VIC, Australia, November 10-13, 2025, Proceedings, Part II, Lecture Notes in Computer Science, pages 35-50. Springer, 2025. URL: https://doi.org/10.1007/978-3-031-95976-9_3.
  12. Hannes Ihalainen, Andy Oertel, Yong Kiam Tan, Jeremias Berg, Matti Järvisalo, Magnus O. Myreen, and Jakob Nordström. Certified maxsat preprocessing. In Christoph Benzmüller, Marijn J. H. Heule, and Renate A. Schmidt, editors, Automated Reasoning - 12th International Joint Conference, IJCAR 2024, Nancy, France, July 3-6, 2024, Proceedings, Part I, Lecture Notes in Computer Science, pages 396-418. Springer, 2024. URL: https://doi.org/10.1007/978-3-031-63498-7_24.
  13. Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, and Marc Vinyals. Practically feasible proof logging for pseudo-boolean optimization. In Maria Garcia de la Banda, editor, 31st International Conference on Principles and Practice of Constraint Programming, CP 2025, Glasgow, Scotland, August 10-15, 2025, LIPIcs, pages 21:1-21:27. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL: https://doi.org/10.4230/LIPIcs.CP.2025.21.
  14. Peter Lammich. Efficient verified (UN)SAT certificate checking. J. Autom. Reason., 64(3):513-532, 2020. URL: https://doi.org/10.1007/S10817-019-09525-Z.
  15. George L. Nemhauser and Laurence A. Wolsey. Integer and Combinatorial Optimization. Wiley interscience series in discrete mathematics and optimization. Wiley, 1988. URL: https://doi.org/10.1002/9781118627372.
  16. Arnold Neumaier and Oleg Shcherbina. Safe bounds in linear and mixed-integer linear programming. Math. Program., 99(2):283-296, 2004. URL: https://doi.org/10.1007/S10107-003-0433-3.
  17. Alexander Schrijver. Theory of linear and integer programming. Wiley-Interscience series in discrete mathematics and optimization. Wiley, 1999. Google Scholar
  18. Yong Kiam Tan, Marijn J. H. Heule, and Magnus O. Myreen. cake_lpr: Verified propagation redundancy checking in cakeml. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II, Lecture Notes in Computer Science, pages 223-241. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-72013-1_12.
  19. Kenan Wood, Runtian Zhou, Haoze Wu, Hammurabi Mendes, and Jonad Pulaj. Satisfiability modulo theories for verifying MILP certificates. J. Symb. Comput., 135:102543, 2026. URL: https://doi.org/10.1016/J.JSC.2025.102543.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact