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.2022.25
URN: urn:nbn:de:0030-drops-166548
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16654/
Go to the corresponding LIPIcs Volume Portal

Gocht, Stephan ; McCreesh, Ciaran ; Nordström, Jakob

An Auditable Constraint Programming Solver

pdf-format:
LIPIcs-CP-2022-25.pdf (0.6 MB)

Abstract

We describe the design and implementation of a new constraint programming solver that can produce an auditable record of what problem was solved and how the solution was reached. As well as a solution, this solver provides an independently verifiable proof log demonstrating that the solution is correct. This proof log uses the VeriPB proof system, which is based upon cutting planes reasoning with extension variables. We explain how this system can support global constraints, variables with large domains, and reformulation, despite not natively understanding any of these concepts.

BibTeX - Entry

@InProceedings{gocht_et_al:LIPIcs.CP.2022.25,
  author =	{Gocht, Stephan and McCreesh, Ciaran and Nordstr\"{o}m, Jakob},
  title =	{{An Auditable Constraint Programming Solver}},
  booktitle =	{28th International Conference on Principles and Practice of Constraint Programming (CP 2022)},
  pages =	{25:1--25:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-240-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{235},
  editor =	{Solnon, Christine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16654},
  URN =		{urn:nbn:de:0030-drops-166548},
  doi =		{10.4230/LIPIcs.CP.2022.25},
  annote =	{Keywords: Constraint programming, proof logging, auditable solving}
}

Keywords: Constraint programming, proof logging, auditable solving
Collection: 28th International Conference on Principles and Practice of Constraint Programming (CP 2022)
Issue Date: 2022
Date of publication: 23.07.2022
Supplementary Material: Source code for the solver described in this paper can be found here:
Software (Source Code): https://doi.org/10.5281/zenodo.6514093

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