Document Open Access Logo

Formally Verified Certification of Constraint Programming Proofs

Authors Maarten Flippo , Konstantin Sidorov , Tip ten Brink, Clément Pit-Claudel , Emir Demirović

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2026.24.pdf
  • Filesize: 0.97 MB
  • 23 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • Constraint programming
  • Proof systems
  • Certified checking

Metrics

Abstract

As constraint programming (CP) solvers are increasingly used in critical applications, there is a growing need for certification of solver claims of infeasibility and optimality. Recent work has demonstrated that certification is feasible for CP solvers using a multi-stage proof-generation framework; however, the underlying proof system was informal, and verification relied on translation into an external proof format, impacting the trustworthiness. We address these issues by formalising a rigorous, solver-agnostic framework for certifying CP solver claims. We present a formal definition of DRCP, a proof system for CP over integer domains that captures core solver operations, including conflict analysis and heterogeneous propagation, by modular inference rules with precise semantics. We also develop FznDrcpCheck, a formally verified proof checker in Rocq that validates DRCP proofs directly against FlatZinc models. Our evaluation shows that our framework enables practical certification across various benchmarks with negligible overhead during solving and modest proof-checking costs.

Cite As Get BibTex

Maarten Flippo, Konstantin Sidorov, Tip ten Brink, Clément Pit-Claudel, and Emir Demirović. Formally Verified Certification of Constraint Programming Proofs. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 24:1-24:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.CP.2026.24

Author Details

Maarten Flippo
  • Delft University of Technology, The Netherlands
Konstantin Sidorov
  • Delft University of Technology, The Netherlands
Tip ten Brink
  • Delft University of Technology, The Netherlands
Clément Pit-Claudel
  • EPFL, Lausanne, Switzerland
Emir Demirović
  • Delft University of Technology, The Netherlands

Funding

  • Flippo, Maarten: Supported by the project "Towards a Unification of AI-Based Solving Paradigms for Combinatorial Optimisation" (OCENW.M.21.078) of the research programme "Open Competition Domain Science - M" which is financed by the Dutch Research Council (NWO).
  • Sidorov, Konstantin: Supported by the TU Delft AI Labs program as part of the XAIT lab.

Supplementary Materials

References

  1. Abderrahmane Aggoun and Nicolas Beldiceanu. Extending chip in order to solve complex scheduling and placement problems. Mathematical and computer modelling, pages 57-73, 1993. URL: https://doi.org/10.1016/0895-7177(93)90068-a.
  2. Özgür Akgün, Ian P Gent, Christopher Jefferson, Ian Miguel, and Peter Nightingale. Metamorphic testing of constraint solvers. In John Hooker, editor, Principles and practice of constraint programming, pages 727-736, Cham, 2018. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-98334-9_46.
  3. Philippe Baptiste, Claude Le Pape, and Wim Nuijten. Satisfiability tests and time-bound adjustments for cumulative scheduling problems. Annals of operations research, pages 305-333, 1999. URL: https://doi.org/10.1023/a:1018995000688.
  4. Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. cvc5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors, Tools and algorithms for the construction and analysis of systems, pages 415-442, Cham, 2022. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-99524-9_24.
  5. Haniel Barbosa, Andrew Reynolds, Gereon Kremer, Hanna Lachnitt, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Arjun Viswanathan, Scott Viteri, Yoni Zohar, Cesare Tinelli, and Clark Barrett. Flexible proof production in an industrial-strength SMT solver. In Automated reasoning: 11th international joint conference, IJCAR 2022, pages 15-35, Berlin, Heidelberg, 2022. Springer-Verlag. URL: https://doi.org/10.1007/978-3-031-10769-6_3.
  6. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified dominance and symmetry breaking for combinatorial optimisation. The journal of artificial intelligence research, 77:1539-1589, 2023. URL: https://doi.org/10.1613/jair.1.14296.
  7. Matthieu Carlier, Catherine Dubois, and Arnaud Gotlieb. A Certified Constraint Solver over Finite Domains. In Dimitra Giannakopoulou and Dominique Méry, editors, FM 2012: Formal Methods, Lecture Notes in Computer Science, pages 116-131, Berlin, Heidelberg, 2012. Springer. URL: https://doi.org/10.1007/978-3-642-32759-9_12.
  8. Kevin K H Cheung, Ambros M Gleixner, and Daniel E Steffy. Verifying integer programming results. In Friedrich Eisenbrand and Jochen Könemann, editors, Integer programming and combinatorial optimization - 19th international conference, IPCO 2017, volume 10328 of Lecture Notes in Computer Science, pages 148-160, Cham, 2017. Springer. URL: https://doi.org/10.1007/978-3-319-59250-3_13.
  9. Luís Cruz-Filipe, Marijn J H Heule, Warren A Hunt, Jr, Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In Leonardo de Moura, editor, Automated deduction - CADE 26, volume 10395 of Lecture notes in computer science, pages 220-236, Cham, 2017. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-63046-5_14.
  10. Leonardo de Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In C R Ramakrishnan and Jakob Rehof, editors, Tools and algorithms for the construction and analysis of systems, Lecture notes in computer science, pages 337-340, Berlin, Heidelberg, 2008. Springer. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  11. Delft High Performance Computing Centre (DHPC). DelftBlue Supercomputer (Phase 2). https://www.tudelft.nl/dhpc/ark:/44463/DelftBluePhase2, 2024.
  12. Thibaut Feydy and Peter J. Stuckey. Lazy Clause Generation Reengineered. In Ian P. Gent, editor, Principles and Practice of Constraint Programming - CP 2009, volume 5732, pages 352-366. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009. URL: https://doi.org/10.1007/978-3-642-04244-7_29.
  13. Maarten Flippo, Konstantin Sidorov, Imko Marijnissen, Jeff Smits, and Emir Demirović. A multi-stage proof logging framework to certify the correctness of CP solvers. In 30th international conference on principles and practice of constraint programming (CP 2024), pages 11:1-11:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2024. URL: https://doi.org/10.4230/LIPIcs.CP.2024.11.
  14. Graeme Gange, Geoffrey Chu, and Peter Stuckey. Certifying optimality in constraint programming. Unpublished, 2017. Google Scholar
  15. Xavier Gillard, Pierre Schaus, and Yves Deville. SolverCheck: Declarative testing of constraints. In Principles and practice of constraint programming (CP 2019), Lecture notes in computer science, pages 565-582, Cham, 2019. Springer International Publishing. URL: https://doi.org/10.1007/978-3-030-30048-7_33.
  16. Stephan Gocht, Ciaran McCreesh, Magnus O Myreen, Jakob Nordström, Andy Oertel, and Yong Kiam Tan. End-to-end verification for subgraph solving. In Proceedings of the AAAI conference on artificial intelligence, volume 38, pages 8038-8047, 2024. URL: https://doi.org/10.1609/aaai.v38i8.28642.
  17. Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. An auditable constraint programming solver. In 28th international conference on principles and practice of constraint programming (CP 2022), Leibniz International Proceedings in Informatics (LIPIcs). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CP.2022.25.
  18. P Hall. On representatives of subsets. In Classic papers in combinatorics, pages 58-62. Birkhäuser Boston, Boston, MA, 2009. URL: https://doi.org/10.1007/978-0-8176-4842-8_4.
  19. Marijn J.H. Heule, Warren A. Hunt, and Nathan Wetzler. Trimming while checking clausal proofs. In 2013 Formal Methods in Computer-Aided Design, pages 181-188, October 2013. URL: https://doi.org/10.1109/FMCAD.2013.6679408.
  20. George Katsirelos. Generalized NoGoods in CSPs. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 5, pages 390-396, 2005. Google Scholar
  21. Ramana Kumar, Magnus O Myreen, Michael Norrish, and Scott Owens. CakeML: A verified implementation of ML. In Principles of Programming Languages (POPL), pages 179-191. ACM Press, 2014. URL: https://doi.org/10.1145/2535838.2535841.
  22. Peter Lammich. Efficient verified (UN)SAT certificate checking. Journal of automated reasoning, 64(3):513-532, 2020. URL: https://doi.org/10.1007/s10817-019-09525-z.
  23. Arnaud Letort, Nicolas Beldiceanu, and Mats Carlsson. A scalable sweep algorithm for the cumulative constraint. In Michela Milano, editor, Principles and practice of constraint programming, pages 439-454, Berlin, Heidelberg, 2012. Springer. URL: https://doi.org/10.1007/978-3-642-33558-7_33.
  24. Kimbal Marriott and Peter Stuckey. Programming with constraints: An introduction. The MIT Press, 1998. URL: https://doi.org/10.7551/mitpress/5625.001.0001.
  25. Matthew McIlree and Ciaran McCreesh. Certifying bounds propagation for integer multiplication constraints. In 39th annual AAAI conference on artificial intelligence (AAAI'25), pages 11309-11317, Philadelphia, 2025. Association for the Advancement of Artificial Intelligence (AAAI). URL: https://doi.org/10.1609/aaai.v39i11.33230.
  26. Matthew J McIlree and Ciaran McCreesh. Proof logging for smart extensional constraints. In Roland H C Yap, editor, 29th international conference on principles and practice of constraint programming (CP 2023), volume 280 of Leibniz International Proceedings in Informatics (LIPIcs), pages 26:1-26:17, Dagstuhl, Germany, 2023. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CP.2023.26.
  27. Matthew J McIlree, Ciaran McCreesh, and Jakob Nordström. Proof logging for the circuit constraint. In Bistra Dilkina, editor, Integration of constraint programming, artificial intelligence, and operations research, pages 38-55, Cham, 2024. Springer Nature Switzerland. URL: https://doi.org/10.1007/978-3-031-60599-4_3.
  28. Gioni Mexi, Dominik Kamp, Yuji Shinano, Shanwen Pu, Alexander Hoen, Ksenia Bestuzheva, Christopher Hojny, Matthias Walter, Marc E Pfetsch, Sebastian Pokutta, and Thorsten Koch. State-of-the-art methods for pseudo-boolean solving with SCIP. arXiv [math.OC], 2025. URL: https://doi.org/10.48550/arXiv.2501.03390.
  29. Rodrigo Otoni, Martin Blicha, Patrick Eugster, Antti E J Hyvärinen, and Natasha Sharygina. Theory-specific proof steps witnessing correctness of SMT executions. In 2021 58th ACM/IEEE design automation conference (DAC), pages 541-546, 2021. URL: https://doi.org/10.1109/DAC18074.2021.9586272.
  30. Pierre Ouellet and Claude-Guy Quimper. Time-table extended-edge-finding for the cumulative constraint. In Christian Schulte, editor, Principles and practice of constraint programming, pages 562-577, Berlin, Heidelberg, 2013. Springer. URL: https://doi.org/10.1007/978-3-642-40627-0_42.
  31. Tobias Paxian and Armin Biere. Uncovering and classifying bugs in MaxSAT solvers through fuzzing and delta debugging. In Matti Järvisalo and Daniel Le Berre, editors, Proceedings of the 14th international workshop on pragmatics of SAT, pages 59-71. CEUR Workshop Proceedings, 2023. URL: https://ceur-ws.org/Vol-3545/paper5.pdf.
  32. Francesca Rossi, Peter van Beek, and Toby Walsh, editors. Handbook of constraint programming. Foundations of artificial intelligence. Elsevier Science, London, England, 2006. URL: https://doi.org/10.1016/s1574-6526(06)x8001-x.
  33. Konrad Slind and Michael Norrish. A brief overview of HOL4. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem proving in higher order logics, pages 28-32, Berlin, Heidelberg, 2008. Springer. URL: https://doi.org/10.1007/978-3-540-71067-7_6.
  34. Peter J. Stuckey, Thibaut Feydy, Andreas Schutt, Guido Tack, and Julien Fischer. The MiniZinc Challenge 2008-2013. AI Magazine, 35(2):55-60, June 2014. URL: https://doi.org/10.1609/AIMAG.V35I2.2539.
  35. The Coq Development Team. The Coq proof assistant, 2024. URL: https://doi.org/10.5281/zenodo.14542673.
  36. Michael Veksler and Ofer Strichman. A proof-producing CSP solver. In Proceedings of the AAAI conference on artificial intelligence, pages 204-209. Association for the Advancement of Artificial Intelligence (AAAI), 2010. URL: https://doi.org/10.1609/aaai.v24i1.7543.
  37. Nathan Wetzler, Marijn J H Heule, and Warren A Hunt, Jr. DRAT-trim: efficient checking and trimming using expressive clausal proofs. In Carsten Sinz and Uwe Egly, editors, Theory and applications of satisfiability testing - SAT 2014, volume 8561 of Lecture notes in computer science, pages 422-429, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact