2026-07-21T14:12:44Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:19063 2024-03-06T11:03:24Z ddc:004 open_access

Proof Logging for Smart Extensional Constraints McIlree, Matthew J. McCreesh, Ciaran Constraint programming proof logging extensional constraints 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". Schloss Dagstuhl – Leibniz-Zentrum für Informatik Matthew J. McIlree and Ciaran McCreesh 2023 Is Part Of LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2023.26 urn:nbn:de:0030-drops-190633 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.26 eng https://creativecommons.org/licenses/by/4.0/legalcode