Proof Logging for Constraint Programming
2Matthew McIlree (University of Glasgow)
https://simons.berkeley.edu/talks/matthew-mcilree-university-glasgow-2023-04-20
Satisfiability: Theory, Practice, and Beyond
A proof log for a problem-solving algorithm provides a verifiable certificate that the result is correct, and also an auditable record of the steps taken to obtain that result. In the field of Boolean satisfiability, proof-logging has become an expected capability of modern solvers, with a standard proof format, DRAT, widely accepted for independent verification. In contrast, a similar standard practice has not yet been adopted for Constraint Programming (CP), due to the difficulties of applying DRAT to the more expressive formulations and reasoning present in this paradigm. However, recent work towards "An Auditable Constraint Programming Solver" (Gocht et al. 2022) has shown how a proof system working in a pseudo-Boolean format can certify the reasoning carried out for several important expressive global constraints, offering a strong candidate for a complete, general CP proof logging method. This talk will be an introduction to proof logging in the context of constraint programming. It will summarise the main motivations; the core techniques developed so far; and the reasons for being optimistic about the applicability of the method going forward.