Analyzing the numerical correctness of branch-and-bound decisions for mixed-integer programming
Alexander Hoen, Ambros Gleixner
TL;DR
The paper addresses whether the numerical decisions made by floating-point LP-based branch-and-bound solvers for MIPs can be certified as correct in exact arithmetic. It introduces a posteriori verification using a hierarchy of techniques—Safe bounding, Rational reconstruction, Factorization, and Exact LP solving—applied to leaves of the branch-and-bound tree in SCIP/SoPlex. Through experiments on the FPEasy and NumDiff test sets, it shows that the overwhelming majority of decisions are correct in exact arithmetic, with errors affecting only a small number of leaves and often verifiable by fast checks. It discusses implications for using floating-point solvers as grey-box components for exact MIP solving, including partial certificates and directions for extending verification to presolve or cutting planes to approach full exactness.
Abstract
Most state-of-the-art branch-and-bound solvers for mixed-integer linear programming rely on limited-precision floating-point arithmetic and use numerical tolerances when reasoning about feasibility and optimality during their search. While the practical success of floating-point MIP solvers bears witness to their overall numerical robustness, it is well-known that numerically challenging input can lead them to produce incorrect results. Even when their final answer is correct, one critical question remains: Were the individual decisions taken during branch-and-bound justified, i.e., can they be verified in exact arithmetic? In this paper, we attempt a first such a posteriori analysis of a pure LP-based branch-and-bound solver by checking all intermediate decisions critical to the correctness of the result: accepting solutions as integer feasible, declaring the LP relaxation infeasible, and pruning subtrees as subopti mal. Our computational study in the academic MIP solver SCIP confirms the expectation that in the overwhelming majority of cases, all decisions are correct. When errors do occur on numerically challenging instances, they typically affect only a small, typically single-digit, amount of leaf nodes that would require further processing.