An Auditable Constraint Programming Solver
(2022) 28th International Conference on Principles and Practice of Constraint Programming, CP 2022 In Leibniz International Proceedings in Informatics, LIPIcs 235.- 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.
Please use this url to cite or link to this publication:
https://lup.lub.lu.se/record/893f7121-27d7-4734-9f9e-785b46f75ed1
- author
- Gocht, Stephan LU ; McCreesh, Ciaran and Nordström, Jakob LU
- organization
- publishing date
- 2022
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- keywords
- auditable solving, Constraint programming, proof logging
- host publication
- 28th International Conference on Principles and Practice of Constraint Programming, CP 2022
- series title
- Leibniz International Proceedings in Informatics, LIPIcs
- editor
- Solnon, Christine
- volume
- 235
- article number
- 25
- publisher
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik
- conference name
- 28th International Conference on Principles and Practice of Constraint Programming, CP 2022
- conference location
- Haifa, Israel
- conference dates
- 2022-07-31 - 2022-08-08
- external identifiers
-
- scopus:85135696580
- ISSN
- 1868-8969
- ISBN
- 9783959772402
- DOI
- 10.4230/LIPIcs.CP.2022.25
- language
- English
- LU publication?
- yes
- id
- 893f7121-27d7-4734-9f9e-785b46f75ed1
- date added to LUP
- 2022-09-12 12:21:47
- date last changed
- 2023-11-21 11:15:52
@inproceedings{893f7121-27d7-4734-9f9e-785b46f75ed1, abstract = {{<p>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.</p>}}, author = {{Gocht, Stephan and McCreesh, Ciaran and Nordström, Jakob}}, booktitle = {{28th International Conference on Principles and Practice of Constraint Programming, CP 2022}}, editor = {{Solnon, Christine}}, isbn = {{9783959772402}}, issn = {{1868-8969}}, keywords = {{auditable solving; Constraint programming; proof logging}}, language = {{eng}}, publisher = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}}, series = {{Leibniz International Proceedings in Informatics, LIPIcs}}, title = {{An Auditable Constraint Programming Solver}}, url = {{http://dx.doi.org/10.4230/LIPIcs.CP.2022.25}}, doi = {{10.4230/LIPIcs.CP.2022.25}}, volume = {{235}}, year = {{2022}}, }