文章基本信息

标题：Weighted Model Counting on the GPU by Exploiting Small Treewidth
本地全文：下载
作者：Johannes K. Fichte ; Markus Hecher ; Stefan Woltran 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2018
卷号：112
页码：1-16
DOI：10.4230/LIPIcs.ESA.2018.28
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Parameterized Algorithms; Weighted Model Counting; General Purpose Computing on Graphics Processing Units; Dynamic Programming; Tree Decompositions; T