Verifying Integer Programming Results
Kevin K. H. Cheung, Ambros Gleixner, Daniel E. Steffy

TL;DR
This paper introduces a simple, verifiable certificate format for MILP solutions to ensure correctness, along with a tool for independent verification, addressing issues of inaccuracy in existing solvers.
Contribution
It proposes a new, straightforward certificate format for MILP results and provides a verification tool, enhancing result reliability and transparency.
Findings
Successfully extended SCIP to generate certificates
Certificates can be verified with simple inference rules
Demonstrated effectiveness on literature MILP instances
Abstract
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 MILP solution algorithms, the ideal form of such a certificate is not entirely clear. This paper proposes such a certificate format, illustrating its capabilities and structure through examples. The certificate format is designed with simplicity in mind and is composed of a list of statements that can be sequentially verified using a limited number of simple yet powerful inference rules. We present a supplementary verification tool for compressing and checking these certificates independently of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
