Certifying the Output of Constraint Programming Solvers Using Proof Logging

Speaker: Matthew McIlree (University of Glasgow) Title: Certifying the Output of Constraint Programming Solvers Using Proof Logging Summary: Constraint programming (CP) is a powerful paradigm for expressing and solving satisfaction and optimisation problems involving finite domain variables and high-level constraints. But the implementation and engineering of CP algorithms can be extremely complex, error-prone, and difficult to test. We are much more likely to trust the output of a solver if it can provide some kind of certificate of correctness via proof logging. The idea here is that, alongside any answer, a solver should produce a “proof” file, which acts both as an auditable record of the steps taken to solve the problem, as well as a mathematical correctness certificate that can be verified by an independent (and trustworthy) proof-checking program. In this talk, I will discuss the current state of research into adding proof logging to CP solvers. I’ll cover how we can prove unsatisfiability and optimality; what makes this different from established proof logging technology for SAT solvers; and the efforts towards devising efficient justification procedures for the huge variety of propagation algorithms available in the modern CP repertoire. Bio: Matthew McIlree is a final-year PhD student at the University of Glasgow, Scotland, supervised by Ciaran McCreesh and working on proof logging for constraint propagation algorithms. He is currently on a two-month visit to Monash University, working with Peter Stuckey and others on new proof logging and verification techniques.