[Back]

J. Fichte, M. Hecher, M. Zisser:
"gpusat2 - An Improved GPU Model Counter";
Talk: SAT 2019 - The 22nd International Conference on Theory and Applications of Satisfiability Testing, Lissabon; 2019-07-07 - 2019-07-12; in: "Pragmatics of SAT 2019 @ SAT 2019", (2019), 1 - 17.

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 implements
the principle of single instructions on multiple threads (SIMT) for parallel programming on a GPU using the vendor-independent programming
framework OpenCL. We introduce a novel architecture that includes
variable data storages and compressing solution parts. We outline results to experiments where we compare the runtime of our system with stateof-the-art model counters on standard benchmark sets for model counting.
In particular, we test also other parallel solvers and the predecessor of gpusat2. One major outcome is that the novel architecture signi cantly improves our solver over its predecessor. As a side result, we observe that state-of-the-art preprocessors allow to produce tree decompositions of signi cantly smaller width.

gpusat2, Improved GPU Model Counter

Project Head Stefan Woltran:
START