An Auditable Constraint Programming Solver

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningfagfællebedømt

Dokumenter

  • Fulltext

    Forlagets udgivne version, 650 KB, PDF-dokument

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.

OriginalsprogEngelsk
Titel28th International Conference on Principles and Practice of Constraint Programming, CP 2022
RedaktørerChristine Solnon
ForlagSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Publikationsdato2022
Artikelnummer25
ISBN (Elektronisk)9783959772402
DOI
StatusUdgivet - 2022
Begivenhed28th International Conference on Principles and Practice of Constraint Programming, CP 2022 - Haifa, Israel
Varighed: 31 jul. 20228 aug. 2022

Konference

Konference28th International Conference on Principles and Practice of Constraint Programming, CP 2022
LandIsrael
ByHaifa
Periode31/07/202208/08/2022
NavnLeibniz International Proceedings in Informatics, LIPIcs
Vol/bind235
ISSN1868-8969

Bibliografisk note

Funding Information:
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 Funding Stephan Gocht: Supported by the Swedish Research Council grant 2016-00782. Ciaran McCreesh: Supported by a Royal Academy of Engineering research fellowship. Jakob Nordström: Supported by the Swedish Research Council grant 2016-00782 and the Independent Research Fund Denmark grant 9040-00389B.

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

ID: 342672568