License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CP.2023.26
URN: urn:nbn:de:0030-drops-190633
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19063/
Go to the corresponding LIPIcs Volume Portal

McIlree, Matthew J. ; McCreesh, Ciaran

Proof Logging for Smart Extensional Constraints

pdf-format:
LIPIcs-CP-2023-26.pdf (0.7 MB)

Abstract

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".

BibTeX - Entry

@InProceedings{mcilree_et_al:LIPIcs.CP.2023.26,
  author =	{McIlree, Matthew J. and McCreesh, Ciaran},
  title =	{{Proof Logging for Smart Extensional Constraints}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{26:1--26:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/19063},
  URN =		{urn:nbn:de:0030-drops-190633},
  doi =		{10.4230/LIPIcs.CP.2023.26},
  annote =	{Keywords: Constraint programming, proof logging, extensional constraints}
}

Keywords: Constraint programming, proof logging, extensional constraints
Collection: 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)
Issue Date: 2023
Date of publication: 22.09.2023
Supplementary Material: Software: https://doi.org/10.5281/zenodo.8132457

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI