57. A proof system for certifying symmetry and optimality reasoning in integer programming
Invited abstract in session WD-3: Mixed Integer Programming II, stream Discrete Optimization.
Wednesday, 12:00 - 13:30Room: C 104
Authors (first author is the speaker)
| 1. | Ambros Gleixner
|
| HTW Berlin | |
| 2. | Jasper van Doornmalen
|
| Department of Mathematics and Computer Science, Eindhoven University of Technology | |
| 3. | Christopher Hojny
|
| TU Eindhoven | |
| 4. | Leon Eifler
|
| Zuse-Institute Berlin (ZIB) |
Abstract
We present a proof system for establishing the correctness of results produced by optimization algorithms, with a focus on mixed-integer programming (MIP). Our system generalizes the seminal work of Bogaerts, Gocht, McCreesh, and Nordström (2022) for binary programs to handle any additional difficulties arising from unbounded and continuous variables, and covers a broad range of solving techniques, including symmetry handling, cutting planes, and presolving reductions. Consistency across all decisions that affect the feasible region is achieved by a pair of transitive relations on the set of solutions, which relies on the newly introduced notion of consistent branching trees. Combined with a series of machine-verifiable derivation rules, the resulting framework offers practical solutions to enhance the trust in integer programming as a methodology for applications where reliability and correctness are key.
Keywords
- Mixed integer nonlinear optimization
Status: accepted
Back to the list of papers