Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

An Auditable Constraint Programming Solver

Gocht, Stephan LU ; McCreesh, Ciaran and Nordström, Jakob LU (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:
author
; and
organization
publishing date
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}},
}