An Auditable Constraint Programming Solver

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Documents

  • Fulltext

    Final published version, 650 KB, PDF document

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.

Original languageEnglish
Title of host publication28th International Conference on Principles and Practice of Constraint Programming, CP 2022
EditorsChristine Solnon
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publication date2022
Article number25
ISBN (Electronic)9783959772402
DOIs
Publication statusPublished - 2022
Event28th International Conference on Principles and Practice of Constraint Programming, CP 2022 - Haifa, Israel
Duration: 31 Jul 20228 Aug 2022

Conference

Conference28th International Conference on Principles and Practice of Constraint Programming, CP 2022
LandIsrael
ByHaifa
Periode31/07/202208/08/2022
SeriesLeibniz International Proceedings in Informatics, LIPIcs
Volume235
ISSN1868-8969

Bibliographical note

Publisher Copyright:
© Stephan Gocht, Ciaran McCreesh, and Jakob Nordström.

    Research areas

  • auditable solving, Constraint programming, proof logging

ID: 342672568