90-XX OPERATIONS RESEARCH, MATHEMATICAL PROGRAMMING
Filtern
Erscheinungsjahr
- 2021 (1)
Dokumenttyp
- ZIB-Report (1)
Sprache
- Englisch (1)
Volltext vorhanden
- ja (1)
Gehört zur Bibliographie
- nein (1)
Schlagworte
- exact rational mixed integer programming (1) (entfernen)
Institut
- AI in Society, Science, and Technology (1) (entfernen)
We describe a general and safe computational framework that provides integer programming results with the degree of certainty that is required for machine-assisted proofs of mathematical theorems.
At its core, the framework relies on a rational branch-and-bound certificate produced by an exact integer programming solver, SCIP, in order to circumvent floating-point roundoff errors present in most state-of-the-art solvers for mixed-integer programs.
The resulting certificates are self-contained and checker software exists that can verify their correctness independently of the integer programming solver used to produce the certificate.
This acts as a safeguard against programming errors that may be present in complex solver software.
The viability of this approach is tested by applying it to finite cases of Chvátal's conjecture, a long-standing open question in extremal combinatorics.
We take particular care to verify also the correctness of the input for this specific problem, using the Coq formal proof assistant.
As a result we are able to provide a first machine-assisted proof that
Chvátal's conjecture holds for all downsets whose union of sets contains seven elements or less.