Validating Mixed-Integer Programming Solvers

Mixed-integer programming (MIP) is a fundamental class of mathematical optimization problems with broad applications in various domains such as finance, engineering, and management science. MIP solvers, software systems that automatically solve MIP problems, serve as the computational backbone for these applications. Given their widespread use, ensuring the correctness of MIP solvers is crucial, as incorrect results, such as falsely determining feasibility or returning incorrect solutions, can lead to serious real-world consequences. Despite its importance, validating the correctness of MIP solvers remains largely unexplored in both theory and practice.

This paper presents the first systematic effort to address this problem. We propose feasibility-driven instance generation, a simple yet effective technique to generate random MIP instances for testing solver correctness. The core idea is to systematically synthesize MIP instances that are provably feasible or infeasible by construction. These instances are then fed to MIP solvers to detect potential bugs. We realize this methodology in Flip. To date, Flip has uncovered 67 confirmed bugs in five widely used MIP solvers, spanning both open-source and commercial systems. Among these, 54 have been promptly fixed by the developers. Our efforts and findings have been well acknowledged by the MIP solver community.

• Software and its engineering → Software testing and debugging.