Proof Logging for Smart Extensional Constraints (Extended Abstract)

Proof Logging for Smart Extensional Constraints (Extended Abstract)

Matthew J. McIlree, Ciaran McCreesh

Proceedings of the Thirty-Third International Joint Conference on Artificial Intelligence
Sister Conferences Best Papers. Pages 8444-8446. https://doi.org/10.24963/ijcai.2024/938

Proof logging provides an auditable way of guaranteeing that a solver has produced a correct answer using sound reasoning. This is standard practice for Boolean satisfiability solving, but for constraint programming, a challenge is that every propagator must be able to justify all inferences it performs. Here we demonstrate how to support proof logging for a wide range of previously uncertified global constraints. We do this by showing how to justify every inference that could be performed by the propagation algorithms for two families of generalised extensional constraint: "Smart Table" and "Regular Language Membership".
Keywords:
Constraint Satisfaction and Optimization: CSO: Constraint programming