4.5 Article

A Safe Computational Framework for Integer Programming Applied to Chvatal's Conjecture

Journal

Publisher

ASSOC COMPUTING MACHINERY
DOI: 10.1145/3485630

Keywords

Exact rational integer programming; verification; extremal combinatorics

Funding

  1. German Federal Ministry of Education and Research (BMBF) [05M14ZAM, 05M20ZBM]

Ask authors/readers for more resources

This paper presents a general and safe computational framework for machine-assisted proofs of mathematical theorems using integer programming. The framework relies on a rational branch-and-bound certificate to avoid floating-point round-off errors and provides checker software to independently verify the correctness of the certificate.
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 round-off 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 Chvatal'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 the first machine-assisted proof that Chvatal's conjecture holds for all downsets whose union of sets contains seven elements or less.

Authors

I am an author on this paper
Click your name to claim this paper and add it to your profile.

Reviews

Primary Rating

4.5
Not enough ratings

Secondary Ratings

Novelty
-
Significance
-
Scientific rigor
-
Rate this paper

Recommended

No Data Available
No Data Available