Title: Certifying the Output of Constraint Programming Solvers Using Proof Logging

Speaker: Matthew McIlree
University of Glasgow

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.

—

SEMINAR: WED 14 MAY 2025 16:00-17:00 (AEST, Melbourne Time)
ZOOM MEETING ID: 873 1557 5255; PASSWORD: 778635