Creative Commons Attribution 4.0 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: https://drops.dagstuhl.de/opus/volltexte/2022/16654/
Gocht, Stephan ; McCreesh, Ciaran ; Nordström, Jakob
An Auditable Constraint Programming Solver
| pdf-format: |
|
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 | |
| Seminar: | 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 |
