Document Open Access Logo

An Auditable Constraint Programming Solver

Authors Stephan Gocht , Ciaran McCreesh , Jakob Nordström

PDF
Thumbnail PDF

File

LIPIcs.CP.2022.25.pdf
  • Filesize: 0.63 MB
  • 18 pages

Document Identifiers

Author Details

Stephan Gocht
  • Lund University, Sweden
  • University of Copenhagen, Denmark
Ciaran McCreesh
  • University of Glasgow, UK
Jakob Nordström
  • University of Copenhagen, Denmark
  • Lund University, Sweden

Funding

  • Gocht, Stephan: Supported by the Swedish Research Council grant 2016-00782.
  • McCreesh, Ciaran: Supported by a Royal Academy of Engineering research fellowship.
  • Nordström, Jakob: Supported by the Swedish Research Council grant 2016-00782 and the Independent Research Fund Denmark grant 9040-00389B.

Cite As Get BibTex

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), Volume 235, pp. 25:1-25:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.CP.2022.25

Abstract

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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Discrete optimization
Keywords
  • Constraint programming
  • proof logging
  • auditable solving

Metrics

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

Supplementary Materials

References

  1. Ö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. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98334-9_46.
  2. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified symmetry and dominance breaking for combinatorial optimisation. In Thirty-Sixth AAAI Conference on Artificial Intelligence, AAAI 2022, 2022. Google Scholar
  3. Samuel R. Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, chapter 7, pages 233-350. IOS Press, 2nd edition, February 2021. Google Scholar
  4. Chiu Wo Choi, Warwick Harvey, J. H. M. Lee, and Peter J. Stuckey. Finite domain bounds consistency revisited. In AI 2006: Advances in Artificial Intelligence, 19th Australian Joint Conference on Artificial Intelligence, Hobart, Australia, December 4-8, 2006, Proceedings, pages 49-58, 2006. URL: https://doi.org/10.1007/11941439_9.
  5. William J. Cook, Collette R. Coullard, and György Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  6. 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. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-63046-5_14.
  7. Jordan Demeulenaere, Renaud Hartert, Christophe Lecoutre, Guillaume Perez, Laurent Perron, Jean-Charles Régin, and Pierre Schaus. Compact-table: Efficiently filtering table constraints with reversible sparse bit-sets. In Michel Rueher, editor, Principles and Practice of Constraint Programming - 22nd International Conference, CP 2016, Toulouse, France, September 5-9, 2016, Proceedings, volume 9892 of Lecture Notes in Computer Science, pages 207-223. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-44953-1_14.
  8. Catherine Dubois. Formally verified constraints solvers: a guided tour. CICM. Invited talk, 2020. Google Scholar
  9. Leon Eifler and Ambros M. Gleixner. A computational status update for exact rational mixed integer programming. In Mohit Singh and David P. Williamson, editors, Integer Programming and Combinatorial Optimization - 22nd International Conference, IPCO 2021, Atlanta, GA, USA, May 19-21, 2021, Proceedings, volume 12707 of Lecture Notes in Computer Science, pages 163-177. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-73879-2_12.
  10. 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, pages 1486-1494. AAAI Press, 2020. URL: https://aaai.org/ojs/index.php/AAAI/article/view/5507.
  11. Ian P. Gent, Ian Miguel, and Peter Nightingale. Generalised arc consistency for the alldifferent constraint: An empirical survey. Artif. Intell., 172(18):1973-2000, 2008. URL: https://doi.org/10.1016/j.artint.2008.10.006.
  12. 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. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30048-7_33.
  13. Stephan Gocht, Ross McBride, Ciaran McCreesh, Jakob Nordström, Patrick Prosser, and James Trimble. Certifying solvers for clique and maximum common (connected) subgraph problems. In Helmut Simonis, editor, Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, Louvain-la-Neuve, Belgium, September 7-11, 2020, Proceedings, volume 12333 of Lecture Notes in Computer Science, pages 338-357. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_20.
  14. Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Subgraph isomorphism meets cutting planes: Solving with certified solutions. In Christian Bessiere, editor, Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, pages 1134-1140. ijcai.org, 2020. URL: https://doi.org/10.24963/ijcai.2020/158.
  15. Stephan Gocht and Jakob Nordström. Certifying parity reasoning efficiently using pseudo-Boolean proofs. In Thirty-Fifth AAAI Conference on Artificial Intelligence, AAAI 2021, Thirty-Third Conference on Innovative Applications of Artificial Intelligence, IAAI 2021, The Eleventh Symposium on Educational Advances in Artificial Intelligence, EAAI 2021, Virtual Event, February 2-9, 2021, pages 3768-3777. AAAI Press, 2021. URL: https://ojs.aaai.org/index.php/AAAI/article/view/16494.
  16. Evguenii I. Goldberg and Yakov Novikov. Verification of proofs of unsatisfiability for CNF formulas. In Design, Automation and Test in Europe Conference (DATE), pages 10886-10891. IEEE Computer Society, 2003. Google Scholar
  17. Warwick Harvey and Joachim Schimpf. Bounds consistency techniques for long linear constraints. In Proceedings of TRICS: Techniques foR Implementing Constraint programming Systems, pages 39-46, 2002. Google Scholar
  18. 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, 2013. URL: http://ieeexplore.ieee.org/document/6679408/.
  19. Marijn Heule, Warren A. Hunt Jr., and Nathan Wetzler. Verifying refutations with extended resolution. In Maria Paola Bonacina, editor, Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings, volume 7898 of Lecture Notes in Computer Science, pages 345-359. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38574-2_24.
  20. Linnea Ingmar and Christian Schulte. Making compact-table compact. 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 210-218. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-98334-9_14.
  21. Evelyn Lamb. Two-hundred-terabyte maths proof is largest ever. Nature, 545:17-18, 2016. Google Scholar
  22. Christophe Lecoutre. STR2: optimized simple tabular reduction for table constraints. Constraints An Int. J., 16(4):341-371, 2011. URL: https://doi.org/10.1007/s10601-011-9107-6.
  23. Ross M. McConnell, Kurt Mehlhorn, Stefan Näher, and Pascal Schweitzer. Certifying algorithms. Comput. Sci. Rev., 5(2):119-161, 2011. URL: https://doi.org/10.1016/j.cosrev.2010.09.009.
  24. Laurent D. Michel, Pierre Schaus, and Pascal Van Hentenryck. MiniCP: a lightweight solver for constraint programming. Math. Program. Comput., 13(1):133-184, 2021. URL: https://doi.org/10.1007/s12532-020-00190-7.
  25. Olga Ohrimenko, Peter J. Stuckey, and Michael Codish. Propagation = lazy clause generation. In Christian Bessiere, editor, Principles and Practice of Constraint Programming - CP 2007, 13th International Conference, CP 2007, Providence, RI, USA, September 23-27, 2007, Proceedings, volume 4741 of Lecture Notes in Computer Science, pages 544-558. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-74970-7_39.
  26. Adrian Rebola-Pardo and Luís Cruz-Filipe. Complete and efficient DRAT proof checking. In Nikolaj Bjørner and Arie Gurfinkel, editors, 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, pages 1-9. IEEE, 2018. URL: https://doi.org/10.23919/FMCAD.2018.8602993.
  27. Olivier Roussel and Vasco M. Manquinho. Input/output format and solver requirements for the competitions of pseudo-Boolean solvers. Revision 2324. Available at http://www.cril.univ-artois.fr/PB16/format.pdf, January 2016.
  28. Peter J. Stuckey. Certifying optimality in constraint programming, February 2019. Talk at KTH Royal Institute of Technology. Google Scholar
  29. Julian R. Ullmann. Partition search for non-binary constraint satisfaction. Inf. Sci., 177(18):3639-3678, 2007. URL: https://doi.org/10.1016/j.ins.2007.03.030.
  30. Allen Van Gelder. Verifying RUP proofs of propositional unsatisfiability. In 10th International Symposium on Artificial Intelligence and Mathematics (ISAIM), 2008. http://isaim2008.unl.edu/index.php?page=proceedings. Google Scholar
  31. 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. AAAI Press, 2010. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI10/paper/view/1754.
  32. Hélène Verhaeghe. The extensional constraint. PhD thesis, Catholic University of Louvain, Louvain-la-Neuve, Belgium, 2021. URL: http://hdl.handle.net/2078.1/252859.
  33. 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. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-09284-3_31.
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 About DROPS Imprint Privacy Contact