Overview Statistic: PDF-Downloads (blue) and Frontdoor-Views (gray)

A Safe Computational Framework for Integer Programming applied to Chvátal's Conjecture

Please always quote using this URN: urn:nbn:de:0297-zib-84444
  • 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.

Download full text files

Export metadata

Author:Leon EiflerORCiD, Ambros GleixnerORCiD, Jonad Pulaj
Document Type:ZIB-Report
Tag:exact rational mixed integer programming; extremal combinatorics
Date of first Publication:2021/10/21
Series (Serial Number):ZIB-Report (21-35)
Accept ✔
Diese Webseite verwendet technisch erforderliche Session-Cookies. Durch die weitere Nutzung der Webseite stimmen Sie diesem zu. Unsere Datenschutzerklärung finden Sie hier.