Document Open Access Logo

Weighted Model Counting on the GPU by Exploiting Small Treewidth

Authors Johannes K. Fichte , Markus Hecher , Stefan Woltran , Markus Zisser

PDF
Thumbnail PDF

File

LIPIcs.ESA.2018.28.pdf
  • Filesize: 0.86 MB
  • 16 pages

Document Identifiers

Author Details

Johannes K. Fichte
  • International Center for Computational Logic, TU Dresden, 01062 Dresden, Germany
Markus Hecher
  • Institute of Logic and Computation, TU Wien, Favoritenstraße 9-11, 1040 Wien, Austria
Stefan Woltran
  • Institute of Logic and Computation, TU Wien, Favoritenstraße 9-11, 1040 Wien, Austria
Markus Zisser
  • Institute of Logic and Computation, TU Wien, Favoritenstraße 9-11, 1040 Wien, Austria

Funding

The work has been supported by the Austrian Science Fund (FWF), Grants Y698 and P26696, and the German Science Fund (DFG), Grant HO 1294/11-1. The first and second author are also affiliated with the University of Potsdam, Germany.

Cite AsGet BibTex

Johannes K. Fichte, Markus Hecher, Stefan Woltran, and Markus Zisser. Weighted Model Counting on the GPU by Exploiting Small Treewidth. In 26th Annual European Symposium on Algorithms (ESA 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 112, pp. 28:1-28:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.ESA.2018.28

Abstract

We propose a novel solver that efficiently finds almost the exact number of solutions of a Boolean formula (#Sat) and the weighted model count of a weighted Boolean formula (WMC) if the treewidth of the given formula is sufficiently small. The basis of our approach are dynamic programming algorithms on tree decompositions, which we engineered towards efficient parallel execution on the GPU. We provide thorough experiments and compare the runtime of our system with state-of-the-art #Sat and WMC solvers. Our results are encouraging in the sense that also complex reasoning problems can be tackled by parameterized algorithms executed on the GPU if instances have treewidth at most 30, which is the case for more than half of counting and weighted counting benchmark instances.

Subject Classification

ACM Subject Classification
  • Theory of computation → Parameterized complexity and exact algorithms
  • Theory of computation → Complexity theory and logic
  • Computer systems organization → Single instruction, multiple data
  • Hardware → Theorem proving and SAT solving
  • Computing methodologies → Graphics processors
Keywords
  • Parameterized Algorithms
  • Weighted Model Counting
  • General Purpose Computing on Graphics Processing Units
  • Dynamic Programming
  • Tree Decompositions
  • Treewidth

Metrics

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

References

  1. Michael Abseher, Nysret Musliu, and Stefan Woltran. htd - a free, open-source framework for (customized) tree decompositions and beyond. In Domenico Salvagnin and Michele Lombardi, editors, Proceedings of the 14th International Conference on Integration of Artificial Intelligence and Operations Research Techniques in Constraint Programming (CPAIOR'17), volume 10335 of Lecture Notes in Computer Science, pages 376-386, Padova, Italy, jun 2017. Springer Verlag. URL: http://dx.doi.org/10.1007/978-3-319-59776-8_30.
  2. Sean Eron Anderson. Bit twiddling hacks. https://graphics.stanford.edu/~seander/bithacks.html, 2009.
  3. Sander Beckers, Gorik De Samblanx, Floris De Smedt, Toon Goedemé, Lars Struyf, and Joost Vennekens. Parallel hybrid SAT solving using OpenCL. In Nico Roos, Mark Winands, and Jos Uiterwijk, editors, Proceedings of the 24th Benelux Conference on Artificial Intelligence (BNAIC'12), pages 11-18, Maastricht, The Netherlands, 2012. Maastricht University. Google Scholar
  4. Hans L. Bodlaender. A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM J. Comput., 25(6):1305-1317, 1996. Google Scholar
  5. Jan Burchard, Tobias Schubert, and Bernd Becker. Laissez-faire caching for parallel #SAT solving. In Marijn Heule and Sean Weaver, editors, Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT'15), volume 9340 of Lecture Notes in Computer Science, pages 46-61, Austin, TX, USA, 2015. Springer Verlag. URL: http://dx.doi.org/10.1007/978-3-319-24318-4_5.
  6. Jan Burchard, Tobias Schubert, and Bernd Becker. Distributed parallel #sat solving. In Bronis R. de Supinski, editor, Proceedings of the 2016 IEEE International Conference on Cluster Computing (CLUSTER'16), pages 326-335, 2016. URL: http://dx.doi.org/10.1109/CLUSTER.2016.20.
  7. Supratik Chakraborty, Daniel J. Fremont, Kuldeep S. Meel, Sanjit A. Seshia, and Moshe Y. Vardi. Distribution-aware sampling and weighted model counting for SAT. In Carla E. Brodley and Peter Stone, editors, Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI'14), pages 1722-1730, Québec City, QC, Canada, 2014. The AAAI Press. Google Scholar
  8. Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. Improving approximate counting for probabilistic inference: From linear to logarithmic sat solver calls. In Subbarao Kambhampati, editor, Proceedings of 25th International Joint Conference on Artificial Intelligence (IJCAI'16), pages 3569-3576, New York City, NY, USA, jul 2016. The AAAI Press. URL: https://bitbucket.org/kuldeepmeel/approxmc.
  9. Günther Charwat and Stefan Woltran. Dynamic programming-based QBF solving. In Florian Lonsing and Martina Seidl, editors, Proceedings of the 4th International Workshop on Quantified Boolean Formulas (QBF'16), volume 1719, pages 27-40. CEUR Workshop Proceedings (CEUR-WS.org), 2016. co-located with 19th International Conference on Theory and Applications of Satisfiability Testing (SAT'16). Google Scholar
  10. Arthur Choi, Guy Van den Broeck, and Adnan Darwiche. Tractable learning for structured probability spaces: A case study in learning preference distributions. In Qiang Yang, editor, Proceedings of 24th International Joint Conference on Artificial Intelligence (IJCAI'15). The AAAI Press, 2015. Google Scholar
  11. Alessandro Dal Palu, Agostino Dovier, Andrea Formisano, and Enrico Pontelli. Cud@SAT: SAT solving on GPUs. Journal of Experimental &Theoretical Artificial Intelligence, 27(3), 2015. Google Scholar
  12. Adnan Darwiche. New advances in compiling CNF to decomposable negation normal form. In Ramon López De Mántaras and Lorenza Saitta, editors, Proceedings of the 16th European Conference on Artificial Intelligence (ECAI'04), pages 318-322, Valencia, Spain, 2004. IOS Press. Google Scholar
  13. Adnan Darwiche. SDD: A new canonical representation of propositional knowledge bases. In Toby Walsh, editor, Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI'11), pages 819-826, Barcelona, Catalonia, Spain, jul 2011. AAAI Press/IJCAI. Google Scholar
  14. 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, Proceedings of the 12th International Symposium on Parameterized and Exact Computation (IPEC'17), Leibniz International Proceedings in Informatics (LIPIcs), pages 30:1 - -30:13. Dagstuhl Publishing, 2017. URL: http://dx.doi.org/10.4230/LIPIcs.IPEC.2017.30.
  15. Carmel Domshlak and Jörg Hoffmann. Probabilistic planning via heuristic forward search and weighted model counting. Journal of Artificial Intelligence Research, 30, 2007. URL: http://dx.doi.org/10.1613/jair.2289.
  16. Leonardo Dueñas-Osorio, Kuldeep S. Meel, Roger Paredes, and Moshe Y. Vardi. Counting-based reliability estimation for power-transmission grids. In Satinder P. Singh and Shaul Markovitch, editors, Proceedings of the Thirty-First AAAI Conference on Artificial Intelligence (AAAI'17), pages 4488-4494, San Francisco, CA, USA, feb 2017. The AAAI Press. Google Scholar
  17. Stefano Ermon, Carla P. Gomes, and Bart Selman. Uniform solution sampling using a constraint solver as an oracle. In Nando de Freitas and Kevin Murphy, editors, Proceedings of the 28th Conference on Uncertainty in Artificial Intelligence (UAI'12), pages 255-264, Catalina Island, CA, USA, aug 2012. AUAI Press. Google Scholar
  18. Johannes K. Fichte, Markus Hecher, Michael Morak, and Stefan Woltran. Answer set solving with bounded treewidth revisited. In Marcello Balduccini and Tomi Janhunen, editors, Proceedings of the 14th International Conference on Logic Programming and Nonmonotonic Reasoning (LPNMR'17), volume 10377 of Lecture Notes in Computer Science, pages 132-145, Espoo, Finland, jul 2017. Springer Verlag. URL: http://dx.doi.org/10.1007/978-3-319-61660-5_13.
  19. Johannes K. Fichte, Markus Hecher, Stefan Woltran, and Markus Zisser. A Benchmark Collection of #SAT Instances and Tree Decompositions (Benchmark Set), 2018. URL: http://dx.doi.org/10.5281/zenodo.1299752.
  20. Johannes K. Fichte, Markus Hecher, Stefan Woltran, and Markus Zisser. Analyzed Benchmarks and Raw Data on Experiments for gpusat (Dataset), jun 2018. URL: http://dx.doi.org/10.5281/zenodo.1299742.
  21. Johannes K. Fichte, Neha Lodha, and Stefan Szeider. Sat-based local improvement for finding tree decompositions of small width. In Serge Gaspers and Toby Walsh, editors, Proceedings on the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT'17), pages 401-411, Melbourne, VIC, Australia, aug 2017. Springer Verlag. URL: http://dx.doi.org/10.1007/978-3-319-66263-3_25.
  22. Ferdinando Fioretto, Enrico Pontelli, William Yeoh, and Rina Dechter. Accelerating exact and approximate inference for (distributed) discrete optimization with GPUs. Constraints, 23(1):1-23, 2017. URL: http://dx.doi.org/10.1007/s10601-017-9274-1.
  23. Philippe Flajolet. Approximate counting: A detailed analysis. BIT Numerical Mathematics, 25(1):113-134, 1985. URL: http://dx.doi.org/10.1007/BF01934993.
  24. Hironori Fujii and Noriyuki Fujimoto. Gpu acceleration of bcp procedure for sat algorithms. In Hamid R. Arabnia, Hiroshi Ishii, Minoru Ito Kazuki Joe, and Hiroaki Nishikawa, editors, Proceedings of the 24th International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'12), pages 10-16, Las Vegas, NV, USA, 2012. CSREA Press. Google Scholar
  25. Martin Gebser, Benjamin Kaufmann, and Torsten Schaub. Conflict-driven answer set solving: From theory to practice. Artificial Intelligence, 187-188:52-89, 2012. URL: http://dx.doi.org/10.1016/j.artint.2012.04.001.
  26. Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Chapter 20: Model counting. In Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 185 of Frontiers in Artificial Intelligence and Applications, pages 633-654. IOS Press, Amsterdam, Netherlands, 2009. URL: http://dx.doi.org/10.3233/978-1-58603-929-5-633.
  27. Torbjörn Granlund, Gunnar Sjödin, Hans Riesel, Richard Stallman, Brian Beuning, Doug Lea, Paul Zimmermann, Ken Weber, Per Bothner, Joachim Hollman, Bennet Yee, Andreas Schwab, Robert Harley, David Seal, Torsten Ekedahl, Linus Nordberg, Kevin Ryde, Kent Boortz, Steve Root, Gerardo Ballabio, Jason Moxham, Niels Möller, Alberto Zanoni, Marco Bodrato, David Harvey, Martin Boij, Marc Glisse, David S Miller, Mark Sofroniou, and Ulrich Weigand. The GNU multiple precision arithmetic library. https://gmplib.org, 2016.
  28. Norman P. Jouppi, Cliff Young, Nishant Patil, David Patterson, Gaurav Agrawal, Raminder Bajwa, Sarah Bates, Suresh Bhatia, Nan Boden, Al Borchers, Rick Boyle, Pierre-luc Cantin, Clifford Chao, Chris Clark, Jeremy Coriell, Mike Daley, Matt Dau, Jeffrey Dean, Ben Gelb, Tara Vazir Ghaemmaghami, Rajendra Gottipati, William Gulland, Robert Hagmann, C. Richard Ho, Doug Hogberg, John Hu, Robert Hundt, Dan Hurt, Julian Ibarz, Aaron Jaffey, Alek Jaworski, Alexander Kaplan, Harshit Khaitan, Daniel Killebrew, Andy Koch, Naveen Kumar, Steve Lacy, James Laudon, James Law, Diemthu Le, Chris Leary, Zhuyuan Liu, Kyle Lucke, Alan Lundin, Gordon MacKean, Adriana Maggiore, Maire Mahony, Kieran Miller, Rahul Nagarajan, Ravi Narayanaswami, Ray Ni, Kathy Nix, Thomas Norrie, Mark Omernick, Narayana Penukonda, Andy Phelps, Jonathan Ross, Matt Ross, Amir Salek, Emad Samadiani, Chris Severn, Gregory Sizikov, Matthew Snelham, Jed Souter, Dan Steinberg, Andy Swing, Mercedes Tan, Gregory Thorson, Bo Tian, Horia Toma, Erick Tuttle, Vijay Vasudevan, Richard Walter, Walter Wang, Eric Wilcox, and Doe Hyun Yoon. In-datacenter performance analysis of a tensor processing unit. In David Brooks, editor, Proceedings of the 44th International Symposium on Computer Architecture (ISCA'17), pages 1-12, Toronto, ON, Canada, jun 2017. URL: http://dx.doi.org/10.1145/3079856.3080246.
  29. Ton Kloks. Treewidth. Computations and Approximations, volume 842 of Lecture Notes in Computer Science. Springer Verlag, 1994. URL: http://dx.doi.org/10.1007/BFb0045375.
  30. Frédéric Koriche, Jean-Marie Lagniez, Pierre Marquis, and Samuel Thomas. Knowledge compilation for model counting: Affine decision trees. In Francesca Rossi and Sebastian Thrun, editors, Proceedings of the 23rd International Joint Conference on Artificial Intelligence (IJCAI'13), Beijing, China, aug 2013. The AAAI Press. Google Scholar
  31. Jean-Marie Lagniez, Emmanuel Lonca, and Pierre Marquis. Improving model counting by leveraging definability. In Subbarao Kambhampati, editor, Proceedings of 25th International Joint Conference on Artificial Intelligence (IJCAI'16), pages 751-757, New York City, NY, USA, 2016. The AAAI Press. Google Scholar
  32. Jean-Marie Lagniez and Pierre Marquis. Preprocessing for propositional model counting. In Carla E. Brodley and Peter Stone, editors, Proceedings of the 28th AAAI Conference on Artificial Intelligence (AAAI'14), pages 2688-2694, Québec City, QC, Canada, 2014. The AAAI Press. Google Scholar
  33. Jean-Marie Lagniez and Pierre Marquis. An improved decision-DDNF compiler. In Carles Sierra, editor, Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI'17), pages 667-673, Melbourne, VIC, Australia, 2017. The AAAI Press. Google Scholar
  34. Norbert Manthey. Towards next generation sequential and parallel SAT solvers. KI - Kuenstliche Intelligenz, 30(3-4):339-342, 2016. URL: http://dx.doi.org/10.1007/s13218-015-0406-8.
  35. Sheila A. Muise, Christian J .and McIlraith, J. Christopher Beck, and Eric I. Hsu. Dsharp: Fast d-DNNF compilation with sharpSAT. In Leila Kosseim and Diana Inkpen, editors, Proceedings of the 25th Canadian Conference on Artificial Intelligence (AI'17), volume 7310 of Lecture Notes in Computer Science, pages 356-361, Toronto, ON, Canada, 2012. Springer Verlag. URL: http://dx.doi.org/10.1007/978-3-642-30353-1_36.
  36. Umut Oztok and Adnan Darwiche. A top-down compiler for sentential decision diagrams. In Qiang Yang and Michael Wooldridge, editors, Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI'15), pages 3141-3148. The AAAI Press, 2015. Google Scholar
  37. Jonathan Passerat-Palmbach and David Hill. OpenCL: A suitable solution to simplify and unify high performance computing developments, chapter 8. Saxe-Coburg Publications, 2013. Google Scholar
  38. Dan Roth. On the hardness of approximate reasoning. Artificial Intelligence, 82(1-2), 1996. URL: http://dx.doi.org/10.1016/0004-3702(94)00092-1.
  39. Sigve Hortemo Sæther, Jan Arne Telle, and Martin Vatshelle. Solving #SAT and MAXSAT by dynamic programming. Journal of Artificial Intelligence Research, 54:59-82, 2015. Google Scholar
  40. Marko Samer and Stefan Szeider. Algorithms for propositional model counting. Journal of Discrete Algorithms, 8(1):50 - -64, 2010. URL: http://dx.doi.org/10.1016/j.jda.2009.06.002.
  41. Tian Sang, Fahiem Bacchus, Paul Beame, Henry Kautz, and Toniann Pitassi. Combining component caching and clause learning for effective model counting. In Holger H. Hoos and David G. Mitchell, editors, Online Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing (SAT'04), Vancouver, BC, Canada, 2004. Google Scholar
  42. Tian Sang, Paul Beame, and Henry Kautz. Performing bayesian inference by weighted model counting. In Manuela M. Veloso and Subbarao Kambhampati, editors, Proceedings of the 29th National Conference on Artificial Intelligence (AAAI'05). The AAAI Press, 2005. Google Scholar
  43. Marc Stevens, Elie Bursztein, Pierre Karpman, Ange Albertini, and Yarik Markov. The first collision for full sha-1. In Jonathan Katz and Hovav Shacham, editors, Proceedings of the 37th Annual International Cryptology Conference (Advances in Cryptology - CRYPTO'17), volume 10401 of Lecture Notes in Computer Science, pages 570-596, Santa Barbara, CA, USA, 2017. Springer Verlag. URL: http://dx.doi.org/10.1007/978-3-319-63688-7_19.
  44. Marc Thurley. sharpSAT - counting models with advanced component caching and implicit BCP. In Armin Biere and Carla P. Gomes, editors, Proceedings of the 9th International Conference Theory and Applications of Satisfiability Testing (SAT'06), pages 424-429, Seattle, WA, USA, 2006. Springer Verlag. URL: http://dx.doi.org/10.1007/11814948_38.
  45. Takahis Toda and Takehide Soh. Implementing efficient all solutions SAT solvers. ACM Journal of Experimental Algorithmics, 21:1.12, 2015. Special Issue SEA 2014, Regular Papers and Special Issue ALENEX 2013. Google Scholar
  46. Tom C. van der Zanden and Hans L. Bodlaender. Computing treewidth on the GPU. In Daniel Lokshtanov and Naomi Nishimura, editors, Proceedings of the 12th International Symposium on Parameterized and Exact Computation (IPEC'17), volume 89 of Leibniz International Proceedings in Informatics (LIPIcs), pages 29:1-29:13, Dagstuhl, Germany, 2018. Dagstuhl Publishing. URL: http://dx.doi.org/10.4230/LIPIcs.IPEC.2017.29.
  47. Yexiang Xue, Arthur Choi, and Adnan Darwiche. Basing decisions on sentences in decision diagrams. In Jörg Hoffmann and Bart Selman, editors, Proceedings of the 26th AAAI Conference on Artificial Intelligence (AAAI'12), Toronto, ON, Canada, 2012. The AAAI Press. Google Scholar
  48. Moshe Zadka and Guido van Rossum. PEP 237 - unifying long integers and integers. https://www.python.org/dev/peps/pep-0237/, 2001.
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