2026-07-21T20:32:10Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:26675 2026-07-13T14:00:38Z ddc:004 open_access

Proof Logging for Projected Enumeration (and Counting?) Problems in VeriPB McCreesh, Ciaran Nordström, Jakob Oertel, Andy Tan, Yong Kiam Constraint programming proof logging auditable solving When a certifying solver claims that a solution is optimal or that a problem is unsatisfiable, it demonstrates this convincingly by giving a proof log which can be checked by an independent (and ideally formally verified) proof checker. Such an approach should also be viable for enumeration problems ("I have listed all solutions explicitly") and counting problems ("there are exactly 42 solutions"), but the currently most popular proof logging systems contain several vital features which are incompatible with this goal. We explain how the VeriPB system can be modified for enumeration and counting proofs whilst retaining as much as possible of its powerful "strengthening" and "deletion" features. We implement this extension both inside VeriPB’s user-friendly proof checker and elaborator and the formally verified CakePB backend, and use this to obtain formally verified enumerations of solutions for a range of constraint solving and graph problem instances. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ciaran McCreesh and Jakob Nordström and Andy Oertel and Yong Kiam Tan 2026 Is Part Of LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2026.43 urn:nbn:de:0030-drops-266759 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.43 eng https://creativecommons.org/licenses/by/4.0/legalcode