MIAO seminar Mon May 26 at 10:00 CET with Matthew McIlree: Certifying the output of constraint programming solvers using proof logging

5 views
Skip to first unread message

Jakob Nordström

unread,
May 18, 2025, 6:20:47 PM5/18/25
to Constraint solving mailing list
Dear colleagues,

This is just to let you know that on Monday May 26 at 10:00 CET we are happy to present a seminar with Matthew McIlree from the University of Glasgow, who will give a talk titled "Certifying the output of constraint programming solvers using proof logging". You find the abstract at the bottom of this message.

This will be a video seminar at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://youtube.com/@MIAOresearch for people who would like to hear the talk but cannot attend.

More information about the MIAO seminar series can be found at https://jakobnordstrom.se/miao-seminars/.

Best regards,
Jakob Nordström

**********

Monday May 26 at 10:00 (note the time!) on Zoom
Certifying the output of constraint programming solvers using proof logging
(Matthew McIlree, University of Glasgow)

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.

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.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se

Reply all
Reply to author
Forward
0 new messages