6104
eng
reportzib
0
--
2016-11-20
--
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.
1438-0064
urn:nbn:de:0297-zib-61044
10.1007/978-3-319-59250-3_13
F. Eisenbrand and J. Koenemann, eds., Integer Programming and Combinatorial Optimization: 19th International Conference, IPCO 2017
Kevin K. H. Cheung
Ambros Gleixner
Ambros Gleixner
Daniel Steffy
ZIB-Report
16-58
eng
uncontrolled
correctness, verification, proof, certificate, optimality, infeasibility, mixed-integer linear programming
OPERATIONS RESEARCH, MATHEMATICAL PROGRAMMING
Mixed integer programming
Mathematical Optimization
Mathematical Optimization Methods
Gleixner, Ambros
ASTfSCM
MIP-ZIBOPT
MODAL-SynLab
Siemens
MODAL-Gesamt
https://opus4.kobv.de/opus4-zib/files/6104/ZR-16-58.pdf
https://opus4.kobv.de/opus4-zib/files/6104/ZR-16-58-revised.pdf