Document Open Access Logo

Proof Logging for Smart Extensional Constraints

Authors Matthew J. McIlree , Ciaran McCreesh

PDF
Thumbnail PDF

File

LIPIcs.CP.2023.26.pdf
  • Filesize: 0.74 MB
  • 17 pages

Document Identifiers

Author Details

Matthew J. McIlree
  • University of Glasgow, UK
Ciaran McCreesh
  • University of Glasgow, UK

Funding

Part of this work was done while the authors were participating in a programme at the Simons Institute for the Theory of Computing.
  • McCreesh, Ciaran: Supported by a Royal Academy of Engineering research fellowship.

Acknowledgements

The authors would like to thank Jakob Nordström for several helpful discussions regarding pseudo-Boolean encodings and unit propagation.

Cite AsGet BibTex

Matthew J. McIlree and Ciaran McCreesh. Proof Logging for Smart Extensional Constraints. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 26:1-26:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CP.2023.26

Abstract

Proof logging provides an auditable way of guaranteeing that a solver has produced a correct answer using sound reasoning. This is standard practice for Boolean satisfiability solving, but for constraint programming, a challenge is that every propagator must be able to justify all inferences it performs. Here we demonstrate how to support proof logging for a wide range of previously uncertified global constraints. We do this by showing how to justify every inference that could be performed by the propagation algorithms for two families of generalised extensional constraint: "Smart Table" and "Regular Language Membership".

Subject Classification

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

Metrics

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

Supplementary Materials

References

  1. Fahiem Bacchus. GAC Via Unit Propagation. In Christian Bessière, editor, Principles and Practice of Constraint Programming endash CP 2007, Lecture Notes in Computer Science, pages 133-147, Berlin, Heidelberg, 2007. Springer. URL: https://doi.org/10.1007/978-3-540-74970-7_12.
  2. Seulkee Baek, Mario Carneiro, and Marijn J. H. Heule. A flexible proof format for SAT solver-elaborator communication. In Tools and Algorithms for the Construction and Analysis of Systems: 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 – April 1, 2021, Proceedings, Part I, pages 59-75, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-72016-2_4.
  3. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified Symmetry and Dominance Breaking for Combinatorial Optimisation, March 2022. URL: https://doi.org/10.48550/arXiv.2203.12275.
  4. Frédéric Boussemart, Christophe Lecoutre, and Cédric Piette. XCSP3: an integrated format for benchmarking combinatorial constrained problems. CoRR, abs/1611.03398, 2016. URL: https://arxiv.org/abs/1611.03398.
  5. 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.
  6. W. Cook, C.R. Coullard, and Gy. 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.
  7. Luís Cruz-Filipe, Marijn J. H. Heule, Warren A. Hunt, Matt Kaufmann, and Peter Schneider-Kamp. Efficient certified RAT verification. In Leonardo de Moura, editor, Automated Deduction - CADE 26, pages 220-236, Cham, 2017. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-63046-5_14.
  8. Jan Elffers, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Justifying All Differences Using Pseudo-Boolean Reasoning. Proceedings of the AAAI Conference on Artificial Intelligence, 34(02):1486-1494, April 2020. URL: https://doi.org/10.1609/aaai.v34i02.5507.
  9. Stephan Gocht. Certifying Correctness for Combinatorial Algorithms by Using Pseudo-Boolean Reasoning. PhD thesis, Lund University, Sweden, 2022. URL: https://lup.lub.lu.se/record/3550cb96-83d5-4fc7-9e62-190083a3c10a.
  10. Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. An Auditable Constraint Programming Solver. In Christine Solnon, editor, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022), volume 235 of Leibniz International Proceedings in Informatics (LIPIcs), pages 25:1-25:18, Dagstuhl, Germany, 2022. Schloss Dagstuhl endash Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CP.2022.25.
  11. E. Goldberg and Y. Novikov. Verification of proofs of unsatisfiability for cnf formulas. In 2003 Design, Automation and Test in Europe Conference and Exhibition, pages 886-891, 2003. URL: https://doi.org/10.1109/DATE.2003.1253718.
  12. Marijn J. H. Heule, Warren A. Hunt, and Nathan Wetzler. Verifying refutations with extended resolution. In Maria Paola Bonacina, editor, Automated Deduction endash CADE-24, pages 345-359, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-38574-2_24.
  13. 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, 2013. URL: https://doi.org/10.1109/FMCAD.2013.6679408.
  14. Samid Hoda, Willem-Jan van Hoeve, and J. N. Hooker. A systematic approach to MDD-Based constraint programming. In David Cohen, editor, Principles and Practice of Constraint Programming endash CP 2010, pages 266-280, Berlin, Heidelberg, 2010. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-15396-9_23.
  15. Mikael Z Lagerkvist and Gilles Pesant. Modeling irregular shape placement problems with regular constraints. In First workshop on bin packing and placement constraints BPPC’08, 2008. Google Scholar
  16. Jean-Baptiste Mairy, Yves Deville, and Christophe Lecoutre. The Smart Table Constraint. In Laurent Michel, editor, 12th International Conference on Integration of AI and OR Techniques in Constraint Programming (CPAIOR 2015), Lecture Notes in Computer Science, pages 271-287, Cham, 2015. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-18008-3_19.
  17. Ciaran McCreesh and Matthew McIlree. The Glasgow Constraint Solver. GitHub repository, 2023. URL: https://github.com/ciaranm/glasgow-constraint-solver.
  18. 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.
  19. Gilles Pesant. A Regular Language Membership Constraint for Finite Sequences of Variables. In Mark Wallace, editor, 10th International Conference on Principles and Practice of Constraint Programming (CP 2004), Lecture Notes in Computer Science, pages 482-495, Berlin, Heidelberg, 2004. Springer. URL: https://doi.org/10.1007/978-3-540-30201-8_36.
  20. Hélène Verhaeghe. The extensional constraint. PhD thesis, Catholic University of Louvain, Louvain-la-Neuve, Belgium, 2021. Google Scholar
  21. Hélène Verhaeghe, Christophe Lecoutre, Yves Deville, and Pierre Schaus. Extending Compact-Table to Basic Smart Tables. In J. Christopher Beck, editor, Principles and Practice of Constraint Programming, volume 10416, pages 297-307. Springer International Publishing, Cham, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_19.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact