Verification of results returned from mixed-integer linear programming (MILP) solvers is particularly desirable in the context of highly sensitive applications such as hardware verification, compiler optimization, or experimental mathematics. We present an approach for validating proof certificates in the VIPR format (generated for MILP problems) via Satisfiability Modulo Theories (SMT) solvers. The resulting checker is based on the equivalence between the correctness of a VIPR certificate and the satisfiability of a formula in the theory of linear/integer real arithmetic encoded as an SMT instance. We demonstrate the effectiveness of this approach and its variations by evaluating them on existing benchmark instances.

It is well known that reformulating the original problem can be crucial for the performance of mixed-integer programming (MIP) solvers. To ensure correctness, all transformations must preserve the fea sibility status and optimal value of the problem, but there is currently no established methodology to express and verify the equivalence of two mixed-integer programs. In this work, we take a first step in this direction by showing how the correctness of MIP presolve reductions on 0-1 integer linear programs can be certified by using (and suitably extending) the VeriPB tool for pseudo-Boolean proof logging. Our experimental evaluation on both decision and optimization instances demonstrates the computational viability of the approach and leads to suggestions for future revisions of the proof format that will help to reduce the verbosity of the certificates and to accelerate the certification and verification process further.

Goodman established in 1959 that asymptotically 1/4 of all triangles in a two-coloring of the edges of a complete graph are monochromatic. By using the semidefinite programming method of Flag Algebras, we generalize this result to four-colored complete graphs resulting in the tight bound of 1/256. This is the largest Flag Algebra based computation performed to date. We will introduce the basic theory of Flag Algebra semidefinite programming and highlight our new methods such as symmetry decompositions and exact rational LP solving that we used to make this computation possible.