[Zurück]

J. Fichte, M. Hecher, M. Zisser:
"Improved GPU-Based SAT Model Counter";
Vortrag: CP 2019 - Principles and Practice of Constraint Programming - 25th International Conference, Stamford, USA; 30.09.2019 - 04.10.2019; in: "Principles and Practice of Constraint Programming - 25th International Conference, CP 2019", Springer, 11802 (2019), ISBN: 978-3-030-30047-0; S. 491 - 509.

In this paper, we present and evaluate a new parallel propositional
model counter, called gpusat2, which is based on dynamic programming
(DP) on tree decompositions using log-counters. gpusat2 extends its
predecessor by a novel architecture for DP that includes using customized tree decompositions, storing solutions to parts of the input instance during the computation variably in arrays or binary search trees, and compressing solution parts. In addition, we avoid data transfer between the RAM and the VRAM whenever possible and employ extended preprocessing by means of state-of-the-art preprocessors for propositional model counting. Our novel architecture allows gpusat2 to be competitive with modern model counters when we also take preprocessing into consideration. As a side result, we observe that state-of-the-art preprocessors allow to produce tree decompositions of significantly smaller width.

Propositional model counting · Dynamic programming · Parameterized algorithmics · Bounded treewidth

http://dx.doi.org/10.1007/978-3-030-30048-7

Projektleitung Stefan Woltran:
START