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