28 August 2025

Abstract

Constraint programming is a declarative way of solving hard combinatorial, scheduling, resource allocation, and logistics problems. We specify a problem in a high-level language, give it to a solver, and the solver thinks for a while and then gives us the optimal answer. Unfortunately, even the best commercial and academic solvers contain bugs, and will occasionally give a wrong answer, potentially with devastating effects. One way of avoiding this situation is through proof logging, where solvers are modified to output a mathematical proof of correctness alongside their solution. This proof can then be independently audited by a very simple (and potentially even formally verified) proof checking tool, giving us complete confidence in the correctness of solutions (although not the solvers themselves). I’ll explain how proof logging works in general, and give an overview of the challenges and fun involved in bringing it to constraint programming. Ultimately, the aim here is to make algorithms something people can trust with their lives and livelihoods, just as engineers have already done with bridges, planes, and lifts.

Bio

Ciaran McCreesh is a Royal Academy of Engineering Research Fellow working in the Formal Analysis, Theory and Algorithms group in the School of Computing Science at the University of Glasgow. His research looks at practical parallel algorithms, particularly in relation to hard subgraph problems. His publications cover combinatorial search, parallel algorithms, and constraint programming.