# Verifying Integer Programming Results

arXiv: https://arxiv.org/abs/1611.08832 · HTML: https://mlsanity.com/paper/1611.08832/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 27 Nov 2016.

## Built on by (most cited first, 5 of 5)

- [Certified Symmetry and Dominance Breaking for Combinatorial Optimisation](https://mlsanity.com/paper/2203.12275/) (2022)
- [Exact Verification of Graph Neural Networks with Incremental Constraint Solving](https://mlsanity.com/paper/2508.09320/) (2025)
- [How To Discover Short, Shorter, and the Shortest Proofs of Unsatisfiability: A Branch-and-Bound Approach for Resolution Proof Length Minimization](https://mlsanity.com/paper/2411.07955/) (2024)
- [ModelEquivBench: Certifying Multi-Relational Evaluation of LLM-Generated Optimization Models](https://mlsanity.com/paper/2607.29431/) (2026)
- [The Refutation Gap: Certifying Both Halves of an Optimality Claim](https://mlsanity.com/paper/2609.20873/) (2026)

## Abstract (arXiv)

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.