Dr. Ambros Gleixner (Zuse Institute Berlin): Towards Verifiable Mixed-Integer Optimization

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. While standard floating-point solvers
yield satisfactory results for a vast majority of applications, there
are cases where provably correct answers are desirable.

In this talk we will start with a short overview of algorithms for
arithmetically exact mixed-integer linear programming. However, 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 optimization results. Due to
the complex nature of state-of-the-art solution algorithms, the ideal
form of such a certificate is not entirely clear. We propose such a
certificate format, illustrating its capabilities and structure
through examples. The certificate format is designed for easy
verification and is composed of a list of statements that can be
sequentially verified using a limited number of simple yet powerful
inference rules.

Finally, 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 solver
SCIP to produce such certificates.