An Auditable Constraint Programming Solver Article Swipe

View

Related Concepts

Computer science Programming language Solver Constraint programming Constraint (computer-aided design) Parallel computing Mathematics Mathematical optimization Stochastic programming Geometry

Stephan Gocht , Ciaran McCreesh , Jakob Nordström , Christine Solnon ·

YOU? · · 2022 · Open Access · · DOI: https://doi.org/10.4230/lipics.cp.2022.25 · OA: W4412260531

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.