Proof Step Checking in a Constraint Programming Unsatisfiability Proof Checker
T.M. ten Brink (TU Delft - Electrical Engineering, Mathematics and Computer Science)
Emir Demirović – Mentor (TU Delft - Algorithmics)
B.P. Ahrens – Graduation committee member (TU Delft - Programming Languages)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
Abstract
Constraint Programming (CP) solvers are complex pieces of software with a large surface area for bugs, making it difficult to trust their claims of unsatisfiability or optimality. We make a contribution to the development of a CP unsatisfiability proof checker, which is formally verified in Rocq, by investigating how to develop checkers for individual proof steps. In particular, we develop formally verified checkers that can verify the reasoning performed by alldifferent and cumulative timetable propagators. We also introduce a methodology for supporting other propagators and constraints in the checker. We also contribute a formally verified integer domain representation using what we call perforated intervals. Perforated intervals are designed to efficiently interoperate with atomic constraints, which are at the heart of the CP proof system. They are an important building block for the verification of proof steps that combine previous proof steps to derive new facts, which we also part of our contribution, and are also used in our propagation checkers. Our results demonstrate the feasibility of a CP-native unsatisfiability proof checker and increase the understanding of propagation verification. Our work also provides important building blocks that can be used to support additional constraints and propagators.