Verifying integer programming results
From MaRDI portal
Abstract: 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.
Recommendations
- An exact rational mixed-integer programming solver
- A hybrid branch-and-bound approach for exact rational mixed-integer programming
- Safe bounds in linear and mixed-integer linear programming
- A computational status update for exact rational mixed integer programming
- A computational status update for exact rational mixed integer programming
Cited in
(17)- Safe bounds in linear and mixed-integer linear programming
- Cutting planes for families implying Frankl's conjecture
- A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture
- A computational status update for exact rational mixed integer programming
- A computational status update for exact rational mixed integer programming
- Branch-and-bound solves random binary IPs in poly(n)-time
- Compressing branch-and-bound trees
- Characterizing 3-Sets in Union-Closed Families
- Optimal length cutting plane refutations of integer programs
- Safe and Verified Gomory Mixed-Integer Cuts in a Rational Mixed-Integer Program Framework
- Certified dominance and symmetry breaking for combinatorial optimisation
- Engineering and evaluating multi-objective pseudo-Boolean optimizers
- Analyzing the numerical correctness of branch-and-bound decisions for mixed-integer programming
- Optimal length cutting plane refutations of integer programs
- Compressing branch-and-bound trees
- Satisfiability modulo theories for verifying MILP certificates
- A combinatorial certifying algorithm for linear programming problems with gainfree Leontief substitution systems
Describes a project that uses
Uses Software
This page was built for publication: Verifying integer programming results
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2401153)
