Document Open Access Logo

Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters (Short Paper)

Authors Tuukka Korhonen , Matti Järvisalo

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.8.pdf
  • Filesize: 0.87 MB
  • 11 pages

Document Identifiers

Author Details

Tuukka Korhonen
  • HIIT, Department of Computer Science, University of Helsinki, Finland
Matti Järvisalo
  • HIIT, Department of Computer Science, University of Helsinki, Finland

Funding

Work financially supported by Academy of Finland under grants 322869 and 328718.

Cite AsGet BibTex

Tuukka Korhonen and Matti Järvisalo. Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 8:1-8:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.8

Abstract

Propositional model counting (#SAT), the problem of determining the number of satisfying assignments of a propositional formula, is the archetypical #P-complete problem with a wide range of applications in AI. In this paper, we show that integrating tree decompositions of low width into the decision heuristics of a reference exact model counter (SharpSAT) significantly improves its runtime performance. In particular, our modifications to SharpSAT (and its derivant GANAK) lift the runtime efficiency of SharpSAT to the extent that it outperforms state-of-the-art exact model counters, including earlier-developed model counters that exploit tree decompositions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Constraint and logic programming
Keywords
  • propositional model counting
  • decision heuristics
  • tree decompositions
  • empirical evaluation

Metrics

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

Supplementary Materials

References

  1. Fahiem Bacchus, Shannon Dalmao, and Toniann Pitassi. Algorithms and complexity results for #SAT and Bayesian inference. In 44th Symposium on Foundations of Computer Science, FOCS 2003, pages 340-351. IEEE Computer Society, 2003. URL: https://doi.org/10.1109/SFCS.2003.1238208.
  2. Fabrizio Biondi, Michael A. Enescu, Annelie Heuser, Axel Legay, Kuldeep S. Meel, and Jean Quilbeuf. Scalable approximation of quantitative information flow in programs. In Isil Dillig and Jens Palsberg, editors, Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, volume 10747 of Lecture Notes in Computer Science, pages 71-93. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-73721-8_4.
  3. Bernhard Bliem and Matti Järvisalo. Centrality heuristics for exact model counting. In 31st IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2019, pages 59-63. IEEE, 2019. URL: https://doi.org/10.1109/ICTAI.2019.00017.
  4. Hans L. Bodlaender. Discovering treewidth. In Peter Vojtás, Mária Bieliková, Bernadette Charron-Bost, and Ondrej Sýkora, editors, SOFSEM 2005: Theory and Practice of Computer Science, 31st Conference on Current Trends in Theory and Practice of Computer Science, volume 3381 of Lecture Notes in Computer Science, pages 1-16. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-30577-4_1.
  5. Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172(6-7):772-799, 2008. URL: https://doi.org/10.1016/j.artint.2007.11.002.
  6. Adnan Darwiche. Decomposable negation normal form. Journal of the ACM, 48(4):608-647, 2001. URL: https://doi.org/10.1145/502090.502091.
  7. Adnan Darwiche. New advances in compiling CNF into decomposable negation normal form. In Ramón López de Mántaras and Lorenza Saitta, editors, Proceedings of the 16th European Conference on Artificial Intelligence, ECAI'2004, pages 328-332. IOS Press, 2004. Google Scholar
  8. Adnan Darwiche. The C2D compiler user manual. Technical Report D-147, UCLA Department of Computer Science, 2005. Google Scholar
  9. Rina Dechter and Robert Mateescu. AND/OR search spaces for graphical models. Artificial Intelligence, 171(2-3):73-106, 2007. URL: https://doi.org/10.1016/j.artint.2006.11.003.
  10. Holger Dell, Christian Komusiewicz, Nimrod Talmon, and Mathias Weller. The PACE 2017 parameterized algorithms and computational experiments challenge: The second iteration. In Daniel Lokshtanov and Naomi Nishimura, editors, 12th International Symposium on Parameterized and Exact Computation, IPEC 2017, volume 89 of LIPIcs, pages 30:1-30:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.IPEC.2017.30.
  11. Jeffrey M. Dudek, Vu Phan, and Moshe Y. Vardi. ADDMC: Weighted model counting with algebraic decision diagrams. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, pages 1468-1476. AAAI Press, 2020. URL: https://aaai.org/ojs/index.php/AAAI/article/view/5505.
  12. Jeffrey M. Dudek, Vu H. N. Phan, and Moshe Y. Vardi. DPMC: Weighted model counting by dynamic programming on project-join trees. In Helmut Simonis, editor, Principles and Practice of Constraint Programming - 26th International Conference, CP 2020, volume 12333 of Lecture Notes in Computer Science, pages 211-230. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_13.
  13. Aurélie Favier, Simon de Givry, and Philippe Jégou. Exploiting problem structure for solution counting. In Ian P. Gent, editor, Principles and Practice of Constraint Programming - CP 2009, 15th International Conference, CP 2009, volume 5732 of Lecture Notes in Computer Science, pages 335-343. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-04244-7_27.
  14. Johannes K. Fichte, Markus Hecher, and Florim Hamiti. The Model Counting Competition 2020. CoRR, abs/2012.01323, 2020. URL: http://arxiv.org/abs/2012.01323.
  15. Johannes Klaus Fichte, Markus Hecher, and Markus Zisser. An improved GPU-based SAT model counter. In Thomas Schiex and Simon de Givry, editors, Principles and Practice of Constraint Programming - 25th International Conference, CP 2019, volume 11802 of Lecture Notes in Computer Science, pages 491-509. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-30048-7_29.
  16. Michael Hamann and Ben Strasser. Graph bisection with pareto optimization. ACM Journal of Experimental Algorithmics, 23, 2018. URL: https://doi.org/10.1145/3173045.
  17. Markus Hecher, Patrick Thier, and Stefan Woltran. Taming high treewidth with abstraction, nested dynamic programming, and database technology. In Luca Pulina and Martina Seidl, editors, Theory and Applications of Satisfiability Testing - SAT 2020 - 23rd International Conference, volume 12178 of Lecture Notes in Computer Science, pages 343-360. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-51825-7_25.
  18. Philippe Jégou, Hanan Kanso, and Cyril Terrioux. Improving exact solution counting for decomposition methods. In 28th IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2016, pages 327-334. IEEE Computer Society, 2016. URL: https://doi.org/10.1109/ICTAI.2016.0057.
  19. Roberto J. Bayardo Jr. and Joseph Daniel Pehoushek. Counting models using connected components. In Henry A. Kautz and Bruce W. Porter, editors, Proceedings of the Seventeenth National Conference on Artificial Intelligence , AAAI 2000, pages 157-162. AAAI Press / The MIT Press, 2000. URL: http://www.aaai.org/Library/AAAI/2000/aaai00-024.php.
  20. Stefan Kölbl, Gregor Leander, and Tyge Tiessen. Observations on the SIMON block cipher family. In Rosario Gennaro and Matthew Robshaw, editors, Advances in Cryptology - CRYPTO 2015 - 35th Annual Cryptology Conference, volume 9215 of Lecture Notes in Computer Science, pages 161-185. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47989-6_8.
  21. Jean-Marie Lagniez and Pierre Marquis. An improved decision-DNNF compiler. In Carles Sierra, editor, Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence, IJCAI 2017, pages 667-673. ijcai.org, 2017. URL: https://doi.org/10.24963/ijcai.2017/93.
  22. Jean-Marie Lagniez, Pierre Marquis, and Anastasia Paparrizou. Defining and evaluating heuristics for the compilation of constraint networks. In J. Christopher Beck, editor, Principles and Practice of Constraint Programming - 23rd International Conference, CP 2017, volume 10416 of Lecture Notes in Computer Science, pages 172-188. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66158-2_12.
  23. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, DAC 2001, pages 530-535. ACM, 2001. URL: https://doi.org/10.1145/378239.379017.
  24. Umut Oztok and Adnan Darwiche. An exhaustive DPLL algorithm for model counting. Journal of Artificial Intelligence Research, 62:1-32, 2018. URL: https://doi.org/10.1613/jair.1.11201.
  25. Markus N. Rabe, Christoph M. Wintersteiger, Hillel Kugler, Boyan Yordanov, and Youssef Hamadi. Symbolic approximation of the bounded reachability probability in large Markov chains. In Gethin Norman and William H. Sanders, editors, Quantitative Evaluation of Systems - 11th International Conference, QEST 2014, volume 8657 of Lecture Notes in Computer Science, pages 388-403. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10696-0_30.
  26. Neil Robertson and Paul D. Seymour. Graph minors. II. Algorithmic aspects of tree-width. Journal of Algorithms, 7(3):309-322, 1986. URL: https://doi.org/10.1016/0196-6774(86)90023-4.
  27. Marko Samer and Stefan Szeider. Algorithms for propositional model counting. Journal of Discrete Algorithms, 8(1):50-64, 2010. URL: https://doi.org/10.1016/j.jda.2009.06.002.
  28. Tian Sang, Fahiem Bacchus, Paul Beame, Henry A. Kautz, and Toniann Pitassi. Combining component caching and clause learning for effective model counting. In SAT 2004 - The Seventh International Conference on Theory and Applications of Satisfiability Testing, 2004. URL: http://www.satisfiability.org/SAT04/programme/21.pdf.
  29. Tian Sang, Paul Beame, and Henry A. Kautz. Performing Bayesian inference by weighted model counting. In Manuela M. Veloso and Subbarao Kambhampati, editors, The Twentieth National Conference on Artificial Intelligence, AAAI 2005, pages 475-482. AAAI Press / The MIT Press, 2005. URL: http://www.aaai.org/Library/AAAI/2005/aaai05-075.php.
  30. Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilistic exact model counter. In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI 2019, pages 1169-1176. ijcai.org, 2019. URL: https://doi.org/10.24963/ijcai.2019/163.
  31. Fabio Somenzi. CUDD: CU decision diagram package–release 3.0.0, 2015. URL: https://github.com/ivmai/cudd.
  32. Ben Strasser. Computing tree decompositions with FlowCutter: PACE 2017 submission. CoRR, abs/1709.08949, 2017. URL: http://arxiv.org/abs/1709.08949.
  33. Marc Thurley. sharpSAT - counting models with advanced component caching and implicit BCP. In Armin Biere and Carla P. Gomes, editors, Theory and Applications of Satisfiability Testing - SAT 2006, 9th International Conference, volume 4121 of Lecture Notes in Computer Science, pages 424-429. Springer, 2006. URL: https://doi.org/10.1007/11814948_38.
  34. Leslie G. Valiant. The complexity of enumeration and reliability problems. SIAM Journal on Computing, 8(3):410-421, 1979. URL: https://doi.org/10.1137/0208032.
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