Current browse context:
math.CO
Change to browse by:
References & Citations
Mathematics > Combinatorics
Title: A Safe Computational Framework for Integer Programming applied to Chvátal's Conjecture
(Submitted on 5 Sep 2018 (v1), last revised 21 Sep 2020 (this version, v2))
Abstract: 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\'atal'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\'atal's conjecture holds for all downsets whose union of sets contains seven elements or less.
Submission history
From: Leon Eifler [view email][v1] Wed, 5 Sep 2018 15:15:09 GMT (55kb,D)
[v2] Mon, 21 Sep 2020 14:04:54 GMT (57kb)
Link back to: arXiv, form interface, contact.