Weighted Model Counting on the GPU by Exploiting Small Treewidth
From International Center for Computational Logic
Weighted Model Counting on the GPU by Exploiting Small Treewidth
Talk by Johannes Fichte
- Location: APB 3027
- Start: 30. August 2018 at 1:00 pm
- End: 30. August 2018 at 2:30 pm
- Research group: Knowledge Representation and Reasoning
- Research group: Knowledge-Based Systems
- Event series: KBS Seminar
- iCal
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.
- More info at: http://drops.dagstuhl.de/opus/volltexte/2018/9491/
