Document Open Access Logo

Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization

Authors Johannes K. Fichte , Markus Hecher , Valentin Roland

PDF
Thumbnail PDF

File

LIPIcs.CP.2021.24.pdf
  • Filesize: 2.42 MB
  • 20 pages

Document Identifiers

Author Details

Johannes K. Fichte
  • TU Dresden, Germany
Markus Hecher
  • TU Wien, Austria
  • Universität Potsdam, Germany
Valentin Roland
  • TU Dresden, Germany

Funding

  • Fichte, Johannes K.: Google Fellowship at the Simons Institute, UC Berkeley.
  • Hecher, Markus: FWF Grants Y698 and P32830 and Grant WWTF ICT19-065.

Acknowledgements

Authors are given in alphabetical order. Main work has been carried out while the first two authors were visiting the Simons Institute for the Theory of Computing. The authors gratefully acknowledge the valuable comments made by the anonymous reviewers. In particular, the authors thank Roland Yap for his efforts and feedback on the final version of this paper.

Cite AsGet BibTex

Johannes K. Fichte, Markus Hecher, and Valentin Roland. Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CP.2021.24

Abstract

Propositional model counting (MC) and its extensions as well as applications in the area of probabilistic reasoning have received renewed attention in recent years. As a result, also the need for quickly solving counting-based problems with automated solvers is critical for certain areas. In this paper, we present experiments evaluating various techniques in order to improve the performance of parallel model counting on general purpose graphics processing units (GPGPUs). Thereby, we mainly consider engineering efficient algorithms for model counting on GPGPUs that utilize the treewidth of a propositional formula by means of dynamic programming. The combination of our techniques results in the solver GPUSAT3, which is based on the programming framework Cuda that -compared to other frameworks- shows superior extensibility and driver support. When combining all findings of this work, we show that GPUSAT3 not only solves more instances of the recent Model Counting Competition 2020 (MCC 2020) than existing GPGPU-based systems, but also solves those significantly faster. A portfolio with one of the best solvers of MCC 2020 and GPUSAT3 solves 19% more instances than the former alone in less than half of the runtime.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
  • Computing methodologies → Massively parallel algorithms
  • Mathematics of computing → Graph algorithms
Keywords
  • Propositional Satisfiability
  • GPGPU
  • Model Counting
  • Treewidth
  • Tree Decomposition

Metrics

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

Supplementary Materials

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 AI and OR Techniques in Constraint Programming (CPAIOR 2017), Padua, Italy, June 5-8, 2017, volume 10335 of Lecture Notes in Computer Science, pages 376-386. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-59776-8_30.
  2. Stefan Arnborg, Derek G. Corneil, and Andrzej Proskurowski. Complexity of finding embeddings in a k-tree. SIAM Journal on Algebraic Discrete Methods, 8(2):277-284, 1987. URL: https://doi.org/10.1137/0608024.
  3. Fahiem Bacchus, Shannon Dalmao, and Toniann Pitassi. Algorithms and complexity results for #SAT and bayesian inference. In Proceedings of the 44th Symposium on Foundations of Computer Science (FOCS 2003), 11-14 October 2003, Cambridge, MA, USA, pages 340-351. IEEE Computer Soc., 2003. URL: https://doi.org/10.1109/SFCS.2003.1238208.
  4. Hans L. Bodlaender. A linear-time algorithm for finding tree-decompositions of small treewidth. SIAM Journal on Computing, 25(6):1305-1317, 1996. URL: https://doi.org/10.1137/S0097539793251219.
  5. Jan Burchard, Tobias Schubert, and Bernd Becker. Laissez-faire caching for parallel #SAT solving. In Marijn Heule and Sean A. Weaver, editors, Proceedings of the 18th International Conference on Theory and Applications of Satisfiability Testing (SAT 2015), Austin, TX, USA, September 24-27, 2015, volume 9340 of Lecture Notes in Computer Science, pages 46-61. Springer, 2015. Google Scholar
  6. 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 2014), July 27 -31, 2014, Québec City, Québec, Canada, pages 1722-1730. AAAI Press, 2014. URL: http://www.aaai.org/ocs/index.php/AAAI/AAAI14/paper/view/8364.
  7. Supratik Chakraborty, Kuldeep S. Meel, and Moshe Y. Vardi. Algorithmic improvements in approximate counting for probabilistic inference: From linear to logarithmic sat calls. In Subbarao Kambhampati, editor, Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), New York, NY, USA, 9-15 July 2016, pages 3569-3576. IJCAI/AAAI Press, July 2016. URL: http://www.ijcai.org/Abstract/16/503.
  8. Günther Charwat and Stefan Woltran. Expansion-based QBF solving on tree decompositions. Fundamenta Informaticae, 167(1-2):59-92, 2019. URL: https://doi.org/10.3233/FI-2019-1810.
  9. 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 and Michael J. Wooldridge, editors, Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015), Buenos Aires, Argentina, July 25-31, 2015, pages 2861-2868. AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/405.
  10. Shane Cook. CUDA programming: A developer’s guide to parallel computing with GPUs. Applications of GPU Computing Series. Morgan Kaufmann, Boston, 2013. URL: https://doi.org/10.1016/B978-0-12-415933-4.02001-9.
  11. Adnan Darwiche. New advances in compiling CNF to decomposable negation normal form. In Ramón López de Mántaras and Lorenza Saitta, editors, Proceedings of the 16th Eureopean Conference on Artificial Intelligence (ECAI 2004), including Prestigious Applicants of Intelligent Systems, PAIS 2004, Valencia, Spain, August 22-27, 2004, pages 318-322. IOS Press, 2004. Google Scholar
  12. 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 2011), Barcelona, Catalonia, Spain, July 16-22, 2011, pages 819-826. AAAI Press/IJCAI, 2011. URL: https://doi.org/10.5591/978-1-57735-516-8/IJCAI11-143.
  13. 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 2017), September 6-8, 2017, Vienna, Austria, volume 89 of LIPIcs, pages 30:1-30:12. Dagstuhl Publishing, 2017. URL: https://doi.org/10.4230/LIPIcs.IPEC.2017.30.
  14. Carmel Domshlak and Jörg Hoffmann. Probabilistic planning via heuristic forward search and weighted model counting. Journal of Artificial Intelligence Research, 30:565-620, 2007. URL: https://doi.org/10.1613/jair.2289.
  15. Jeffrey M. Dudek, Vu Phan, and Moshe Y. Vardi. ADDMC: weighted model counting with algebraic decision diagrams. In Proceedings of the 34th AAAI Conference on Artificial Intelligence (AAAI 2020), New York, NY, USA, February 7-12, 2020, pages 1468-1476. AAAI Press, 2020. URL: https://aaai.org/ojs/index.php/AAAI/article/view/5505.
  16. 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, Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP 2020), Louvain-la-Neuve, Belgium, September 7-11, 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.
  17. Jeffrey M. Dudek and Moshe Y. Vardi. Parallel weighted model counting with tensor networks. CoRR, abs/2006.15512, 2020. URL: http://arxiv.org/abs/2006.15512.
  18. 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 31st AAAI Conference on Artificial Intelligence (AAAI 2017), February 4-9, 2017, San Francisco, California, USA, pages 4488-4494. AAAI Press, 2017. URL: http://aaai.org/ocs/index.php/AAAI/AAAI17/paper/view/14870.
  19. Naila Farooqui, Andrew Kerr, Gregory Frederick Diamos, Sudhakar Yalamanchili, and Karsten Schwan. A framework for dynamically instrumenting GPU compute applications within GPU ocelot. In Proceedings of the 4th Workshop on General Purpose Processing on Graphics Processing Units (GPGPU 2011), Newport Beach, CA, USA, March 5, 2011, page 9. ACM, 2011. URL: https://doi.org/10.1145/1964179.1964192.
  20. Massimiliano Fatica. Accelerating linpack with CUDA on heterogenous clusters. In David R. Kaeli and Miriam Leeser, editors, Proceedings of the 2nd Workshop on General Purpose Processing on Graphics Processing Units (GPGPU 2009), Washington, DC, USA, March 8, 2009, volume 383 of ACM International Conference Proceeding Series, pages 46-51. ACM, 2009. URL: https://doi.org/10.1145/1513895.1513901.
  21. Johannes K. Fichte and Markus Hecher. The model counting competition 2021. https://mccompetition.org/past_iterations, 2021.
  22. Johannes K. Fichte, Markus Hecher, and Florim Hamiti. The model counting competition 2020. ACM Journal of Experimental Algorithmics, 2021. In press. Google Scholar
  23. Johannes K. Fichte, Markus Hecher, and Arne Meier. Counting complexity for reasoning in abstract argumentation. In Proceedings of the 33rd AAAI Conference on Artificial Intelligence (AAA'19), Honolulu, Hawaii, USA, 2018. Google Scholar
  24. Johannes K. Fichte, Markus Hecher, and Arne Meier. Knowledge-base degrees of inconsistency: Complexity and counting. In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI'21), pages 6349-6357, 2021. Google Scholar
  25. Johannes K. Fichte, Markus Hecher, and Andreas Pfandler. Lower Bounds for QBFs of Bounded Treewidth. In Naoki Kobayashi, editor, Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'20), pages 410-424. Assoc. Comput. Mach., New York, 2020. Google Scholar
  26. Johannes K. Fichte, Markus Hecher, and Valentin Roland. GPUSAT3 benchmark data and source code, 2021. URL: https://doi.org/10.5281/zenodo.5159903.
  27. Johannes K. Fichte, Markus Hecher, Patrick Thier, and Stefan Woltran. Exploiting database management systems and treewidth for counting. In Ekaterina Komendantskaya and Y. Annie Liu, editors, Proceedings of the 22nd International Symposium on Practical Aspects of Declarative Languages (PADL'20), volume 12007 of Lecture Notes in Computer Science, pages 151-167. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-39197-3_10.
  28. Johannes K. Fichte, Markus Hecher, Stefan Woltran, and Markus Zisser. Weighted model counting on the GPU by exploiting small treewidth. In Yossi Azar, Hannah Bast, and Grzegorz Herman, editors, Proceedings of the 26th Annual European Symposium on Algorithms (ESA 2018), August 20-22, 2018, Helsinki, Finland, volume 112 of LIPIcs, pages 28:1-28:16. Dagstuhl Publishing, 2018. URL: https://doi.org/10.4230/LIPIcs.ESA.2018.28.
  29. Johannes K. Fichte, Markus Hecher, and Markus Zisser. An improved GPU-based SAT model counter. In Thomas Schiex and Simon de Givry, editors, Proceedings of the 25th International Conference on Principles and Practice of Constraint Programming (CP 2019), Stamford, CT, USA, September 30 - October 4, 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.
  30. Robert D. Finn, Jody Clements, and Sean R. Eddy. HMMER web server: interactive sequence similarity searching. Nucleic Acids Research, 39(Web-Server-Issue):29-37, 2011. URL: https://doi.org/10.1093/nar/gkr367.
  31. Rong Ge, Ryan Vogt, Jahangir Majumder, Arif Alam, Martin Burtscher, and Ziliang Zong. Effects of dynamic voltage and frequency scaling on a K20 GPU. In Proceedings of the 42nd International Conference on Parallel Processing (ICPP 2013), Lyon, France, October 1-4, 2013, pages 826-833. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/ICPP.2013.98.
  32. GNU Project. GNU libc manual, 3.5.2 locked memory details. URL: https://www.gnu.org/software/libc/manual/html_node/Locked-Memory-Details.html.
  33. Markus Hecher. Treewidth-aware reductions of normal ASP to SAT - is normal ASP harder than SAT after all? In Diego Calvanese, Esra Erdem, and Michael Thielscher, editors, Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning, KR 2020, Rhodes, Greece, September 12-18, 2020, pages 485-495, 2020. URL: https://doi.org/10.24963/kr.2020/49.
  34. 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, Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT 2020), Alghero, Italy, July 3-10, 2020, 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.
  35. Marijn Heule and Hans van Maaren. Parallel SAT solving using bit-level operations. Journal on Satisfiability, Boolean Modeling and Computation, 4(2-4):99-116, 2008. URL: https://doi.org/10.3233/sat190040.
  36. Jared Hoberock, Nathan Bell, and Thrust Contributors. Thrust API documentation. URL: https://thrust.github.io/doc/classthrust_1_1mr_1_1disjoint__unsynchronized__pool__resource.html.
  37. Lukasz Jarzabek and Pawel Czarnul. Performance evaluation of unified memory and dynamic parallelism for selected parallel CUDA applications. Journal of Supercomputing, 73(12):5378-5401, 2017. URL: https://doi.org/10.1007/s11227-017-2091-x.
  38. Jean-Marie Lagniez, Emmanuel Lonca, and Pierre Marquis. Improving model counting by leveraging definability. In Subbarao Kambhampati, editor, Proceedings of the 25th International Joint Conference on Artificial Intelligence (IJCAI 2016), New York, NY, USA, 9-15 July 2016, pages 751-757. The AAAI Press, July 2016. URL: http://www.ijcai.org/Abstract/16/112.
  39. 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 2017), Melbourne, Australia, August 19-25, 2017, pages 667-673. The AAAI Press, 2017. URL: https://doi.org/10.24963/ijcai.2017/93.
  40. Jean-Marie Lagniez, Pierre Marquis, and Nicolas Szczepanski. DMC: a distributed model counter. In Jérôme Lang, editor, Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI 2018), July 13-19, 2018, Stockholm, Sweden, pages 1331-1338. The AAAI Press, 2018. URL: https://doi.org/10.24963/ijcai.2018/185.
  41. Silviu Maniu, Pierre Senellart, and Suraj Jog. An experimental study of the treewidth of real-world graph data. In Pablo Barceló and Marco Calautti, editors, Proceedings of the 22nd International Conference on Database Theory (ICDT 2019), March 26-28, 2019, Lisbon, Portugal, volume 127 of LIPIcs, pages 12:1-12:18. Dagstuhl Publishing, 2019. URL: https://doi.org/10.4230/LIPIcs.ICDT.2019.12.
  42. 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 Advances in Artificial Intelligence Artificial Intelligence (Canadian AI 2012), Toronto, ON, Canada, May 28-30, 2012, volume 7310 of Lecture Notes in Computer Science, pages 356-361. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-30353-1_36.
  43. NVIDIA Corporation. Application note - CUDA 2.2 pinned memory APIs. URL: http://developer.download.nvidia.com/compute/DevZone/C/html/C/src/simpleZeroCopy/doc/CUDA2.2PinnedMemoryAPIs.pdf.
  44. Umut Oztok and Adnan Darwiche. A top-down compiler for sentential decision diagrams. In Qiang Yang and Michael J. Wooldridge, editors, Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015), Buenos Aires, Argentina, July 25-31, 2015, pages 3141-3148. The AAAI Press, 2015. URL: http://ijcai.org/Abstract/15/443.
  45. Saddam Quirem, Fahian Ahmed, and Byeong Kil Lee. CUDA acceleration of P7Viterbi algorithm in HMMER 3.0. In Sheng Zhong, Dejing Dou, and Yu Wang, editors, Proceedings of the 30th IEEE International Performance Computing and Communications Conference (IPCCC 2011), Orlando, Florida, USA, November 17-19, 2011, pages 1-2. IEEE, 2011. URL: https://doi.org/10.1109/PCCC.2011.6108104.
  46. Dan Roth. On the hardness of approximate reasoning. Artificial Intelligence, 82(1-2):273-302, 1996. URL: https://doi.org/10.1016/0004-3702(94)00092-1.
  47. 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.
  48. Tian Sang, Paul Beame, and Henry A. Kautz. Performing bayesian inference by weighted model counting. In Manuela M. Veloso and Subbarao Kambhampati, editors, Proceedings of the 20th National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, July 9-13, 2005, Pittsburgh, Pennsylvania, USA, pages 475-482. AAAI Press / The MIT Press, 2005. URL: http://www.aaai.org/Library/AAAI/2005/aaai05-075.php.
  49. Shubham Sharma, Subhajit Roy, Mate Soos, and Kuldeep S. Meel. GANAK: A scalable probabilistic exact model counter. In Sarit Kraus, editor, Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI 2019), Macao, China, August 10-16, 2019, pages 1169-1176, 2019. URL: https://doi.org/10.24963/ijcai.2019/163.
  50. Ben Strasser. Computing tree decompositions with flowcutter: PACE 2017 submission. CoRR, abs/1709.08949, 2017. URL: http://arxiv.org/abs/1709.08949.
  51. 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 on Theory and Applications of Satisfiability Testing (SAT 2006), Seattle, WA, USA, August 12-15, 2006, volume 4121 of Lecture Notes in Computer Science, pages 424-429. Springer, 2006. URL: https://doi.org/10.1007/11814948_38.
  52. Richard Vuduc and Jee Choi. A Brief History and Introduction to GPGPU, pages 9-23. Springer US, Boston, MA, 2013. URL: https://doi.org/10.1007/978-1-4614-8745-6_2.
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact