Document Open Access Logo

Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms

Authors Emir Demirović , Ciaran McCreesh , Matthew J. McIlree , Jakob Nordström , Andy Oertel , Konstantin Sidorov

PDF

File

Thumbnail PDF
PDF
LIPIcs.CP.2024.9.pdf
  • Filesize: 0.93 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Discrete optimization
Keywords
  • Proof logging
  • dynamic programming
  • decision diagrams

Metrics

Abstract

Pseudo-Boolean proof logging has been used successfully to provide certificates of optimality from a variety of constraint- and satisifability-style solvers that combine reasoning with a backtracking or clause-learning search. Another paradigm, occurring in dynamic programming and decision diagram solving, instead reasons about partial states and possible transitions between them. We describe a framework for generating clean and efficient pseudo-Boolean proofs for these kinds of algorithm, and use it to produce certifying algorithms for knapsack, longest path, and interval scheduling. Because we use a common proof system, we can also reason about hybrid solving algorithms: we demonstrate this by providing proof logging for a dynamic programming based knapsack propagator inside a constraint programming solver.

Cite As Get BibTex

Emir Demirović, Ciaran McCreesh, Matthew J. McIlree, Jakob Nordström, Andy Oertel, and Konstantin Sidorov. Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CP.2024.9

Author Details

Emir Demirović
  • TU Delft, The Netherlands
Ciaran McCreesh
  • University of Glasgow, Scotland
Matthew J. McIlree
  • University of Glasgow, Scotland
Jakob Nordström
  • University of Copenhagen, Denmark
  • Lund University, Sweden
Andy Oertel
  • Lund University, Sweden
  • University of Copenhagen, Denmark
Konstantin Sidorov
  • TU Delft, The Netherlands

Funding

  • Demirović, Emir: part of the XAIT lab funded by the Delft AI Labs programme.
  • McCreesh, Ciaran: supported by a Royal Academy of Engineering research fellowship, and by the Engineering and Physical Sciences Research Council [grant number EP/X030032/1].
  • Nordström, Jakob: supported by the Swedish Research Council grant 2016-00782 and the Independent Research Fund Denmark grant 9040-00389B.
  • Oertel, Andy: supported by the Wallenberg AI, Autonomous Systems and Software Program (WASP) funded by the Knut and Alice Wallenberg Foundation.
  • Sidorov, Konstantin: part of the XAIT lab funded by the Delft AI Labs programme.

Acknowledgements

Part of this work was carried out while taking part in the semester program Satisfiability: Theory, Practice, and Beyond in 2021 at the Simons Institute for the Theory of Computing at UC Berkeley, and in the extended reunion of this semester program in the spring of 2023. This work has also benefited greatly from discussions during the Dagstuhl Seminars 22411 Theory and Practice of SAT and Combinatorial Solving and 23261 SAT Encodings and Beyond.

Supplementary Materials

References

  1. Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, and Dieter Vandesande. Certified core-guided MaxSAT solving. In Brigitte Pientka and Cesare Tinelli, editors, Automated Deduction - CADE 29 - 29th International Conference on Automated Deduction, Rome, Italy, July 1-4, 2023, Proceedings, volume 14132 of Lecture Notes in Computer Science, pages 1-22. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-38499-8_1.
  2. David Bergman, André A. Ciré, Ashish Sabharwal, Horst Samulowitz, Vijay A. Saraswat, and Willem Jan van Hoeve. Parallel combinatorial optimization with decision diagrams. In Helmut Simonis, editor, Integration of AI and OR Techniques in Constraint Programming - 11th International Conference, CPAIOR 2014, Cork, Ireland, May 19-23, 2014. Proceedings, volume 8451 of Lecture Notes in Computer Science, pages 351-367. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-07046-9_25.
  3. David Bergman, André A. Ciré, Willem-Jan van Hoeve, and John N. Hooker. Decision Diagrams for Optimization. Artificial Intelligence: Foundations, Theory, and Algorithms. Springer, 2016. URL: https://doi.org/10.1007/978-3-319-42849-9.
  4. Bart Bogaerts, Stephan Gocht, Ciaran McCreesh, and Jakob Nordström. Certified dominance and symmetry breaking for combinatorial optimisation. J. Artif. Intell. Res., 77:1539-1589, 2023. URL: https://doi.org/10.1613/JAIR.1.14296.
  5. 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.
  6. Randal E. Bryant. Tbuddy: A proof-generating BDD package. In Alberto Griggio and Neha Rungta, editors, 22nd Formal Methods in Computer-Aided Design, FMCAD 2022, Trento, Italy, October 17-21, 2022, pages 49-58. IEEE, 2022. URL: https://doi.org/10.34727/2022/ISBN.978-3-85448-053-2_10.
  7. 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
  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, Waterloo, ON, Canada, June 26-28, 2017, Proceedings, volume 10328 of Lecture Notes in Computer Science, pages 148-160. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-59250-3_13.
  9. 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.
  10. 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.
  11. Torsten Fahle and Meinolf Sellmann. Cost based filtering for the constrained knapsack problem. Ann. Oper. Res., 115(1-4):73-93, 2002. URL: https://doi.org/10.1023/A:1021193019522.
  12. 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.
  13. 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.
  14. 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.
  15. Stephan Gocht, Ciaran McCreesh, Magnus O. Myreen, Jakob Nordström, Andy Oertel, and Yong Kiam Tan. End-to-end verification for subgraph solving. In Michael J. Wooldridge, Jennifer G. Dy, and Sriraam Natarajan, editors, Thirty-Eighth AAAI Conference on Artificial Intelligence, AAAI 2024, Thirty-Sixth Conference on Innovative Applications of Artificial Intelligence, IAAI 2024, Fourteenth Symposium on Educational Advances in Artificial Intelligence, EAAI 2014, February 20-27, 2024, Vancouver, Canada, pages 8038-8047. AAAI Press, 2024. URL: https://doi.org/10.1609/AAAI.V38I8.28642.
  16. 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.
  17. 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, July 31 to August 8, 2022, Haifa, Israel, volume 235 of LIPIcs, pages 25:1-25:18. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPICS.CP.2022.25.
  18. 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://doi.org/10.1609/AAAI.V35I5.16494.
  19. 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: https://ieeexplore.ieee.org/document/6679408/.
  20. 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.
  21. John N. Hooker. Generalized resolution for 0-1 linear inequalities. Ann. Math. Artif. Intell., 6(1-3):271-286, 1992. URL: https://doi.org/10.1007/BF01531033.
  22. John N. Hooker. Decision diagrams and dynamic programming. In Carla P. Gomes and Meinolf Sellmann, editors, Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, 10th International Conference, CPAIOR 2013, Yorktown Heights, NY, USA, May 18-22, 2013. Proceedings, volume 7874 of Lecture Notes in Computer Science, pages 94-110. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38171-3_7.
  23. Toni Jussila, Carsten Sinz, and Armin Biere. Extended resolution proofs for symbolic SAT solving with quantification. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, Seattle, WA, USA, August 12-15, 2006, Proceedings, volume 4121 of Lecture Notes in Computer Science, pages 54-60. Springer, 2006. URL: https://doi.org/10.1007/11814948_8.
  24. Irit Katriel, Meinolf Sellmann, Eli Upfal, and Pascal Van Hentenryck. Propagating knapsack constraints in sublinear time. In Proceedings of the Twenty-Second AAAI Conference on Artificial Intelligence, July 22-26, 2007, Vancouver, British Columbia, Canada, pages 231-236. AAAI Press, 2007. URL: http://www.aaai.org/Library/AAAI/2007/aaai07-035.php.
  25. Antoon W.J. Kolen, Jan Karel Lenstra, Christos H. Papadimitriou, and Frits C.R. Spieksma. Interval scheduling: A survey. Naval Research Logistics (NRL), 54(5):530-543, 2007. URL: https://doi.org/10.1002/nav.20231.
  26. Yuri Malitsky, Meinolf Sellmann, and Radoslaw Szymanek. Filtering bounded knapsack constraints in expected sublinear time. 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, pages 141-146. AAAI Press, 2010. URL: https://doi.org/10.1609/AAAI.V24I1.7560.
  27. Yuri Malitsky, Meinolf Sellmann, and Willem Jan van Hoeve. Length-lex bounds consistency for knapsack constraints. In Peter J. Stuckey, editor, Principles and Practice of Constraint Programming, 14th International Conference, CP 2008, Sydney, Australia, September 14-18, 2008. Proceedings, volume 5202 of Lecture Notes in Computer Science, pages 266-281. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-85958-1_18.
  28. 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.
  29. 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, August 27-31, 2023, Toronto, Canada, volume 280 of LIPIcs, pages 26:1-26:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.CP.2023.26.
  30. Meinolf Sellmann. Approximated consistency for knapsack constraints. In Francesca Rossi, editor, Principles and Practice of Constraint Programming - CP 2003, 9th International Conference, CP 2003, Kinsale, Ireland, September 29 - October 3, 2003, Proceedings, volume 2833 of Lecture Notes in Computer Science, pages 679-693. Springer, 2003. URL: https://doi.org/10.1007/978-3-540-45193-8_46.
  31. Carsten Sinz and Armin Biere. Extended resolution proofs for conjoining bdds. In Dima Grigoriev, John Harrison, and Edward A. Hirsch, editors, Computer Science - Theory and Applications, First International Symposium on Computer Science in Russia, CSR 2006, St. Petersburg, Russia, June 8-12, 2006, Proceedings, volume 3967 of Lecture Notes in Computer Science, pages 600-611. Springer, 2006. URL: https://doi.org/10.1007/11753728_60.
  32. Steven Skiena. The Algorithm Design Manual, Third Edition. Texts in Computer Science. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-54256-6.
  33. Peter J. Stuckey, Kim Marriott, and Guido Tack. The MiniZinc handbook section 4.2.1: Global constraints, 2023. URL: https://www.minizinc.org/doc-2.5.3/en/lib-globals.html.
  34. Michael A. Trick. A dynamic programming approach for consistency and propagation for knapsack constraints. Ann. Oper. Res., 118(1-4):73-84, 2003. URL: https://doi.org/10.1023/A:1021801522545.
  35. 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.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact