{'fraction_non_alphanumeric': 0.01761846901579587, 'fraction_numerical': 0.010328068043742407, 'mean_word_length': 5.215094339622642, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization

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. 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.