Certifying Optimality in Constraint Programming
This is a joint seminar between SCS and Castor .
Speaker: Peter Stuckey, Monash University
Title: Certifying Optimality in Constraint Programming
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.
Joint work with Graeme Gange
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. His research interests include: discrete optimization; programming languages, in particular declarative programing languages; constraint solving algorithms; bioinformatics; and constraint-based graphics. He enjoys problem solving in any area, having publications in e.g. databases, timetabling, and system security, and working with companies such as Oracle and Rio Tinto on problems that interest them.