Verifying integer programming results
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.
|Keywords||Certificate, Correctness, Infeasibility, Mixed-integer linear programming, Optimality, Proof, Verification|
|Series||Lecture Notes in Computer Science|
Cheung, K, Gleixner, A. (Ambros), & Steffy, D.E. (Daniel E.). (2017). Verifying integer programming results. In Lecture Notes in Computer Science. doi:10.1007/978-3-319-59250-3_13