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.
| Original language | English |
|---|---|
| Title of host publication | 28th International Conference on Principles and Practice of Constraint Programming, CP 2022 |
| Editors | Christine Solnon |
| Publisher | Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing |
| Publication date | 2022 |
| Article number | 25 |
| ISBN (Electronic) | 9783959772402 |
| DOIs | |
| Publication status | Published - 2022 |
| Event | 28th International Conference on Principles and Practice of Constraint Programming, CP 2022 - Haifa, Israel Duration: 31 Jul 2022 → 8 Aug 2022 |
Conference
| Conference | 28th International Conference on Principles and Practice of Constraint Programming, CP 2022 |
|---|---|
| Country/Territory | Israel |
| City | Haifa |
| Period | 31/07/2022 → 08/08/2022 |
| Series | Leibniz International Proceedings in Informatics, LIPIcs |
|---|---|
| Volume | 235 |
| ISSN | 1868-8969 |
Bibliographical note
Publisher Copyright:© Stephan Gocht, Ciaran McCreesh, and Jakob Nordström.
Keywords
- auditable solving
- Constraint programming
- proof logging