Fichte, J., Hecher, M., Woltran, S., & Zisser, M. (2018). Weighted Model Counting on the GPU by Exploiting Small Treewidth. In Y. Azar, H. Bast, & G. Herman (Eds.), 26th Annual European Symposium on Algorithms, {ESA} 2018 (pp. 28:2-28:16). Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. https://doi.org/10.4230/LIPIcs.ESA.2018.28
E192-02 - Forschungsbereich Databases and Artificial Intelligence
-
Published in:
26th Annual European Symposium on Algorithms, {ESA} 2018
-
ISBN:
978-3-95977-081-1
-
Date (published):
2018
-
Event name:
European Symposium on Algorithms (ESA)
en
Event date:
20-Aug-2018 - 24-Aug-2018
-
Event place:
Helsinki, Finland
-
Number of Pages:
15
-
Publisher:
Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 112
-
Publisher:
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, Dagstuhl
-
Peer reviewed:
Yes
-
Keywords:
Treewidth; Parameterized Algorithms; Weighted Model Counting; General Pur-pose Computing on Graphics Processing Units; Dynamic Programming; Tree Decompositions
-
Abstract:
We propose a novel solver that eÿciently 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 suÿciently small. The basis of our approach are dynamic programming algorithms on tree decompositions, which we engineered towards eÿcient 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.
en
Project title:
START: Y 698-N23 (Fonds zur Förderung der wissenschaftlichen Forschung (FWF))
-
Research Areas:
außerhalb der gesamtuniversitären Forschungsschwerpunkte: 100%
