  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.

Optimization and Control;Discrete Mathematics;Mathematical Software