Standard
An Auditable Constraint Programming Solver. / Gocht, Stephan; McCreesh, Ciaran; Nordström, Jakob.
28th International Conference on Principles and Practice of Constraint Programming, CP 2022. ed. / Christine Solnon. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2022. 25 (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 235).
Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review
Harvard
Gocht, S, McCreesh, C
& Nordström, J 2022,
An Auditable Constraint Programming Solver. in C Solnon (ed.),
28th International Conference on Principles and Practice of Constraint Programming, CP 2022., 25, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, Leibniz International Proceedings in Informatics, LIPIcs, vol. 235, 28th International Conference on Principles and Practice of Constraint Programming, CP 2022, Haifa, Israel,
31/07/2022.
https://doi.org/10.4230/LIPIcs.CP.2022.25APA
Gocht, S., McCreesh, C.
, & Nordström, J. (2022).
An Auditable Constraint Programming Solver. In C. Solnon (Ed.),
28th International Conference on Principles and Practice of Constraint Programming, CP 2022 [25] Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. Leibniz International Proceedings in Informatics, LIPIcs Vol. 235
https://doi.org/10.4230/LIPIcs.CP.2022.25Vancouver
Gocht S, McCreesh C
, Nordström J.
An Auditable Constraint Programming Solver. In Solnon C, editor, 28th International Conference on Principles and Practice of Constraint Programming, CP 2022. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2022. 25. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 235).
https://doi.org/10.4230/LIPIcs.CP.2022.25Author
Gocht, Stephan ; McCreesh, Ciaran ; Nordström, Jakob. / An Auditable Constraint Programming Solver. 28th International Conference on Principles and Practice of Constraint Programming, CP 2022. editor / Christine Solnon. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2022. (Leibniz International Proceedings in Informatics, LIPIcs, Vol. 235).
Bibtex
@inproceedings{bc72cfac27664d3593a8db54d07b10df,
title = "An Auditable Constraint Programming Solver",
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.",
keywords = "auditable solving, Constraint programming, proof logging",
author = "Stephan Gocht and Ciaran McCreesh and Jakob Nordstr{\"o}m",
note = "Publisher Copyright: {\textcopyright} Stephan Gocht, Ciaran McCreesh, and Jakob Nordstr{\"o}m.; 28th International Conference on Principles and Practice of Constraint Programming, CP 2022 ; Conference date: 31-07-2022 Through 08-08-2022",
year = "2022",
doi = "10.4230/LIPIcs.CP.2022.25",
language = "English",
series = "Leibniz International Proceedings in Informatics, LIPIcs",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",
editor = "Christine Solnon",
booktitle = "28th International Conference on Principles and Practice of Constraint Programming, CP 2022",
}
RIS
TY - GEN
T1 - An Auditable Constraint Programming Solver
AU - Gocht, Stephan
AU - McCreesh, Ciaran
AU - Nordström, Jakob
N1 - Publisher Copyright:
© Stephan Gocht, Ciaran McCreesh, and Jakob Nordström.
PY - 2022
Y1 - 2022
N2 - 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.
AB - 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.
KW - auditable solving
KW - Constraint programming
KW - proof logging
U2 - 10.4230/LIPIcs.CP.2022.25
DO - 10.4230/LIPIcs.CP.2022.25
M3 - Article in proceedings
AN - SCOPUS:85135696580
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 28th International Conference on Principles and Practice of Constraint Programming, CP 2022
A2 - Solnon, Christine
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 28th International Conference on Principles and Practice of Constraint Programming, CP 2022
Y2 - 31 July 2022 through 8 August 2022
ER -
