VIPR

VIPR. Verifying Integer Programming Results. VIPR is new a software project to verify, in exact rational arithmetic, the correctness of results computed by mixed-integer linear programming solvers. It is based on an elementary file format for LP-based branch-and-cut certificates proposed in the article ”Kevin K.H. Cheung, Ambros Gleixner, and Daniel E. Steffy: 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 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 how they were created. We report computational results on a selection of mixed-integer linear programming instances from the literature. To this end, we have extended the exact rational version of the MIP solver SCIP to produce such certificates.