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

[Jakob Nordström]

Dear all,

On Monday May 26 at 10:00 CET (note the time!) 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/ --- in particular, don't miss 
the talks tomorrow Monday May 19 at 14:00 by Artur Riazanov titled "The 
generalised Linial–Nisan conjecture is false for DNFs" and on Tuesday 
May 20 at 14:00 with Kilian Risse titled "Supercritical tradeoffs for 
monotone circuits". If you do not wish to receive these announcements, 
or receive several copies of them, please send a message to jn at di.ku.dk.

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