Document Open Access Logo

A Multi-Stage Proof Logging Framework to Certify the Correctness of CP Solvers

Authors Maarten Flippo , Konstantin Sidorov , Imko Marijnissen , Jeff Smits , Emir Demirović

PDF
Thumbnail PDF

File

LIPIcs.CP.2024.11.pdf
  • Filesize: 1.05 MB
  • 20 pages

Document Identifiers

Author Details

Maarten Flippo
  • Delft University of Technology, The Netherlands
Konstantin Sidorov
  • Delft University of Technology, The Netherlands
Imko Marijnissen
  • Delft University of Technology, The Netherlands
Jeff Smits
  • Delft University of Technology, The Netherlands
Emir Demirović
  • Delft University of Technology, The Netherlands

Funding

Maarten Flippo and Jeff Smits: 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.
  • Marijnissen, Imko: Supported by the NWO/OCW, as part of the Quantum Software Consortium programme (project number 024.003.037 / 3368).

Cite AsGet BibTex

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). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.CP.2024.11

Abstract

Proof logging is used to increase trust in the optimality and unsatisfiability claims of solvers. However, to this date, no constraint programming solver can practically produce proofs without significantly impacting performance, which hinders mainstream adoption. We address this issue by introducing a novel proof generation framework, together with a CP proof format and proof checker. Our approach is to divide the proof generation into three steps. At runtime, we require the CP solver to only produce a proof sketch, which we call a scaffold. After the solving is done, our proof processor trims and expands the scaffold into a full CP proof, which is subsequently verified. Our framework is agnostic to the solver and the verification approach. Through MiniZinc benchmarks, we demonstrate that with our framework, the overhead of logging during solving is often less than 10%, significantly lower than other approaches, and that our proof processing step can reduce the overall size of the proof by orders of magnitude and by extension the proof checking time. Our results demonstrate that proof logging has the potential to become an integral part of the CP community.

Subject Classification

ACM Subject Classification
  • Mathematics of computing → Combinatorial optimization
  • Theory of computation → Logic and verification
Keywords
  • proof logging
  • formal verification
  • constraint programming

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Tobias Achterberg. Constraint Integer Programming. PhD thesis, Technische Universität Berlin, October 2007. Google Scholar
  2. Tobias Achterberg. SCIP: solving constraint integer programs. Math. Program. Comput., 1(1):1-41, July 2009. URL: https://doi.org/10.1007/s12532-008-0001-1.
  3. Abderrahmane Aggoun and Nicolas Beldiceanu. Extending CHIP in order to solve complex scheduling and placement problems. In Jean-Paul Delahaye, Philippe Devienne, Philippe Mathieu, and Pascal Yim, editors, JFPL'92, 1ères Journées Francophones de Programmation Logique, 25-27 Mai 1992, Lille, France, volume 17, page 51, 1992. URL: https://doi.org/10.1016/0895-7177(93)90068-A.
  4. Özgür Akgün, Ian P. Gent, Christopher Jefferson, Ian Miguel, and Peter Nightingale. Metamorphic testing of constraint solvers. In John N. Hooker, editor, Principles and Practice of Constraint Programming - 24th International Conference, CP 2018, Lille, France, August 27-31, 2018, Proceedings, volume 11008 of Lecture Notes in Computer Science, pages 727-736, Cham, 2018. Springer. URL: https://doi.org/10.1007/978-3-319-98334-9_46.
  5. Gilles Audemard, Christophe Lecoutre, and Emmanuel Lonca. Proceedings of the 2023 XCSP3 competition. CoRR, abs/2312.05877, 2023. URL: https://doi.org/10.48550/arXiv.2312.05877.
  6. Tomas Balyo, Marijn Heule, Markus Iser, Matti Järvisalo, and Martin Suda, editors. Proceedings of SAT Competition 2023: Solver, Benchmark and Proof Checker Descriptions. Department of Computer Science Series of Publications B. Department of Computer Science, University of Helsinki, Finland, 2023. Google Scholar
  7. Haniel Barbosa, Clark W. 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 - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, pages 415-442, Cham, 2022. Springer. URL: https://doi.org/10.1007/978-3-030-99524-9_24.
  8. Clark Barrett, Leonardo De Moura, and Pascal Fontaine. Proofs in satisfiability modulo theories. All about proofs, Proofs for all, 55(1):23-44, 2015. Google Scholar
  9. Nicolas Beldiceanu and Mats Carlsson. A new multi-resource cumulatives constraint with negative heights. In Pascal Van Hentenryck, editor, Principles and Practice of Constraint Programming - CP 2002, pages 63-79, Berlin, Heidelberg, 2002. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/3-540-46135-3_5.
  10. Nikolaj S. Bjørner, Clemens Eisenhofer, and Laura Kovács. Satisfiability modulo custom theories in Z3. In Cezara Dragoi, Michael Emmi, and Jingbo Wang, editors, Verification, Model Checking, and Abstract Interpretation - 24th International Conference, VMCAI 2023, Boston, MA, USA, January 16-17, 2023, Proceedings, volume 13881 of Lecture Notes in Computer Science, pages 91-105, Cham, 2023. Springer. URL: https://doi.org/10.1007/978-3-031-24950-1_5.
  11. Miquel Bofill, Jordi Coll, Josep Suy, and Mateu Villaret. Compact mdds for pseudo-boolean constraints with at-most-one relations in resource-constrained scheduling problems. In Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI-17, pages 555-562, 2017. URL: https://doi.org/10.24963/ijcai.2017/78.
  12. Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, and Pascal Fontaine. verit: An open, trustable and efficient smt-solver. In Renate A. Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings, volume 5663 of Lecture Notes in Computer Science, pages 151-156, Berlin, Heidelberg, 2009. Springer. URL: https://doi.org/10.1007/978-3-642-02959-2_12.
  13. Robert Brummayer, Florian Lonsing, and Armin Biere. Automated testing and debugging of SAT and QBF solvers. In Ofer Strichman and Stefan Szeider, editors, Theory and Applications of Satisfiability Testing - SAT 2010, 13th International Conference, SAT 2010, Edinburgh, UK, July 11-14, 2010. Proceedings, volume 6175 of Lecture Notes in Computer Science, pages 44-57, Berlin, Heidelberg, 2010. Springer. URL: https://doi.org/10.1007/978-3-642-14186-7_6.
  14. Sam Buss and Jakob Nordström. Proof complexity and sat solving. Handbook of Satisfiability, 336:233-350, 2021. URL: https://doi.org/10.3233/FAIA200990.
  15. 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 - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, volume 7436 of Lecture Notes in Computer Science, pages 116-131, Berlin, Heidelberg, 2012. Springer. URL: https://doi.org/10.1007/978-3-642-32759-9_12.
  16. 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, Waterloo, ON, Canada, June 26-28, 2017, Proceedings, 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.
  17. Geoffrey Chu, Peter J. Stuckey, Andreas Schutt, Thorsten Ehlers, Graeme Gange, and Kathryn Francis. Chuffed, a lazy clause generation solver. URL: https://github.com/chuffed/chuffed/.
  18. William Cook, Thorsten Koch, Daniel E Steffy, and Kati Wolter. A hybrid branch-and-bound approach for exact rational mixed-integer programming. Mathematical Programming Computation, 5(3):305-344, 2013. URL: https://doi.org/10.1007/s12532-013-0055-6.
  19. 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 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings, volume 10395 of Lecture Notes in Computer Science, pages 220-236, Cham, 2017. Springer. URL: https://doi.org/10.1007/978-3-319-63046-5_14.
  20. Jessica Davies and Fahiem Bacchus. Exploiting the power of mip solvers in maxsat. In International Conference on Theory and Applications of Satisfiability Testing, pages 166-181. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-39071-5_13.
  21. Toby O. Davies, Graeme Gange, and Peter J. Stuckey. Automatic logic-based benders decomposition with minizinc. In Proceedings of the AAAI Conference on Artificial Intelligence, pages 787-793, 2017. URL: https://doi.org/10.1609/aaai.v31i1.10654.
  22. Sven De Vries and Rakesh V Vohra. Combinatorial auctions: A survey. INFORMS Journal on computing, 15(3):284-309, 2003. URL: https://doi.org/10.1287/ijoc.15.3.284.16077.
  23. Delft High Performance Computing Centre (DHPC). DelftBlue Supercomputer (Phase 1). https://www.tudelft.nl/dhpc/ark:/44463/DelftBluePhase1, 2022.
  24. Jan Elffers, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Justifying all differences using pseudo-boolean reasoning. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligence Conference, IAAI 2020, The Tenth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2020, New York, NY, USA, February 7-12, 2020, volume 34, pages 1486-1494. AAAI Press, April 2020. URL: https://doi.org/10.1609/aaai.v34i02.5507.
  25. Thibaut Feydy and Peter J Stuckey. Lazy clause generation reengineered. In International Conference on Principles and Practice of Constraint Programming, pages 352-366. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04244-7_29.
  26. Graeme Gange, Jeremias Berg, Emir Demirović, and Peter J Stuckey. Core-guided and core-boosted search for cp. In Integration of Constraint Programming, Artificial Intelligence, and Operations Research: 17th International Conference, CPAIOR 2020, Vienna, Austria, September 21-24, 2020, Proceedings 17, pages 205-221. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58942-4_14.
  27. Graeme Gange, Geoffrey Chu, and Peter Stuckey. Certifying optimality in constraint programming. unpublished, 2017. URL: https://github.com/gkgange/cert-cp.
  28. Allen Van Gelder. Verifying RUP proofs of propositional unsatisfiability. In International Symposium on Artificial Intelligence and Mathematics, ISAIM 2008, Fort Lauderdale, Florida, USA, January 2-4, 2008, 2008. URL: http://isaim2008.unl.edu/PAPERS/TechnicalProgram/ISAIM2008_0008_60a1f9b2fd607a61ec9e0feac3f438f8.pdf.
  29. Xavier Gillard, Pierre Schaus, and Yves Deville. Solvercheck: Declarative testing of constraints. In Thomas Schiex and Simon de Givry, editors, Principles and Practice of Constraint Programming - 25th International Conference, CP 2019, Stamford, CT, USA, September 30 - October 4, 2019, Proceedings, volume 11802 of Lecture Notes in Computer Science, pages 565-582, Cham, 2019. Springer. URL: https://doi.org/10.1007/978-3-030-30048-7_33.
  30. Stephan Gocht, Ciaran McCreesh, and Jakob Nordstrom. Veripb: The easy way to make your combinatorial search algorithm trustworthy. From Constraint Programming to Trustworthy AI, 2020. Google Scholar
  31. Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. An auditable constraint programming solver. In DROPS-IDN/v2/document/10.4230/LIPIcs.CP.2022.25. Schloss-Dagstuhl - Leibniz Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.CP.2022.25.
  32. Stephan Gocht and Jakob Nordström. Certifying parity reasoning efficiently using pseudo-boolean proofs. Proceedings of the AAAI Conference on Artificial Intelligence, 35(5):3768-3777, May 2021. URL: https://doi.org/10.1609/aaai.v35i5.16494.
  33. Evguenii I. Goldberg and Yakov Novikov. Verification of proofs of unsatisfiability for CNF formulas. In 2003 Design, Automation and Test in Europe Conference and Exposition (DATE 2003), 3-7 March 2003, Munich, Germany, pages 10886-10891. IEEE Computer Society, March 2003. URL: https://doi.org/10.1109/DATE.2003.10008.
  34. Marijn Heule. Schur number five. Proceedings of the AAAI Conference on Artificial Intelligence, 32(11), April 2018. URL: https://doi.org/10.1609/aaai.v32i1.12209.
  35. Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Trimming while checking clausal proofs. In Formal Methods in Computer-Aided Design, FMCAD 2013, Portland, OR, USA, October 20-23, 2013, pages 181-188. IEEE, October 2013. URL: https://doi.org/10.1109/FMCAD.2013.6679408.
  36. Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek. Solving and verifying the boolean pythagorean triples problem via cube-and-conquer. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 228-245, Cham, 2016. Springer. URL: https://doi.org/10.1007/978-3-319-40970-2_15.
  37. John N Hooker and Greger Ottosson. Logic-based benders decomposition. Mathematical Programming, 96(1):33-60, 2003. URL: https://doi.org/10.1007/s10107-003-0375-9.
  38. Joao Marques-Silva, Inês Lynce, and Sharad Malik. Conflict-driven clause learning sat solvers. In Handbook of satisfiability, pages 133-182. ios Press, 2021. URL: https://doi.org/10.3233/FAIA200987.
  39. Nicholas Nethercote, Ralph Stuckey, Peter J. Becket, Sebastian Brand, Gregory J. Duck, and Guido Tac. Minizinc: Towards a standard cp modelling language. In Principles and Practice of Constraint Programming – CP 2007, pages 529-543. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74970-7_38.
  40. Olga Ohrimenko, Peter J Stuckey, and Michael Codish. Propagation via lazy clause generation. Constraints, 14:357-391, 2009. URL: https://doi.org/10.1007/s10601-008-9064-x.
  41. 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 co-located with the 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023), Alghero, Italy, July 4, 2023, volume 3545 of CEUR Workshop Proceedings, pages 59-71. CEUR-WS.org, 2023. URL: https://ceur-ws.org/Vol-3545/paper5.pdf.
  42. Christian Schulte, Mikael Lagerkvist, and Guido Tack. Gecode - generic constraint development environment. URL: https://www.gecode.org/.
  43. João P. Marques Silva and Karem A. Sakallah. GRASP - a new search algorithm for satisfiability. In Rob A. Rutenbar and Ralph H. J. M. Otten, editors, Proceedings of the 1996 IEEE/ACM International Conference on Computer-Aided Design, ICCAD 1996, San Jose, CA, USA, November 10-14, 1996, pages 220-227. IEEE Computer Society / ACM, November 1996. URL: https://doi.org/10.1109/ICCAD.1996.569607.
  44. Guido Tack and Peter J. Stuckey. Minizinc challenge 2023. URL: https://www.minizinc.org/challenge2023/results2023.html.
  45. Michael Veksler and Ofer Strichman. A proof-producing CSP solver. In Maria Fox and David Poole, editors, Proceedings of the Twenty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2010, Atlanta, Georgia, USA, July 11-15, 2010, volume 24, pages 204-209. AAAI Press, July 2010. URL: https://doi.org/10.1609/aaai.v24i1.7543.
  46. Nathan Wetzler, Marijn 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 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 14-17, 2014. Proceedings, volume 8561 of Lecture Notes in Computer Science, pages 422-429, Cham, 2014. Springer. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
  47. Lintao Zhang and Sharad Malik. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In 2003 Design, Automation and Test in Europe Conference and Exposition (DATE 2003), 3-7 March 2003, Munich, Germany, pages 10880-10885. IEEE Computer Society, March 2003. URL: https://doi.org/10.1109/DATE.2003.10014.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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