Certifying Optimality in Constraint Programming

Abstract
Discrete optimization problems are one of the most challenging class of problems to solve, they are typically NP-hard. Complete solving approaches to these problems, such as integer programming or constraint programming, are able to prove optimal solutions. Since complete solvers are highly complex software objects, when a solver returns that it has proved optimality, how confident can we be in this result? The short answer is not very. Constraint programming (CP) solvers can hide difficult to observe bugs because they rely on complex state maintenance over backtracking. In this work we develop a strategy for validating unsatisfiability and optimality results. We extend a lazy clause generation CP solver with proof-generating capabilities, which is paired with an external, formally certified proof checking procedure. From this, we derive several proof checkers, which establish different compromises between trust base and performance. We validate the practicality of this approach by verifying correctness of alleged unsatisfiability and optimality results from the 2016 MiniZinc challenge.


Biography
Professor Peter J. Stuckey is a Professor in the Faculty of Information Technology at Monash University, and project leader in the Data61 CSIRO laboratory. Peter Stuckey is a pioneer in constraint programming, the science of modelling and solving complex combinatorial problems.