License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ESA.2018.28
URN: urn:nbn:de:0030-drops-94915
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2018/9491/
Go to the corresponding LIPIcs Volume Portal

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

Weighted Model Counting on the GPU by Exploiting Small Treewidth

pdf-format:
LIPIcs-ESA-2018-28.pdf (0.9 MB)

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.

BibTeX - Entry

@InProceedings{fichte_et_al:LIPIcs:2018:9491,
  author =	{Johannes K. Fichte and Markus Hecher and Stefan Woltran and Markus Zisser},
  title =	{{Weighted Model Counting on the GPU by Exploiting Small Treewidth}},
  booktitle =	{26th Annual European Symposium on Algorithms (ESA 2018)},
  pages =	{28:1--28:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-081-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{112},
  editor =	{Yossi Azar and Hannah Bast and Grzegorz Herman},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9491},
  URN =		{urn:nbn:de:0030-drops-94915},
  doi =		{10.4230/LIPIcs.ESA.2018.28},
  annote =	{Keywords: Parameterized Algorithms, Weighted Model Counting, General Purpose Computing on Graphics Processing Units, Dynamic Programming, Tree Decompositions, T}
}

Keywords: Parameterized Algorithms, Weighted Model Counting, General Purpose Computing on Graphics Processing Units, Dynamic Programming, Tree Decompositions, T
Collection: 26th Annual European Symposium on Algorithms (ESA 2018)
Issue Date: 2018
Date of publication: 14.08.2018

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI