Talks and Poster Presentations (with Proceedings-Entry):

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.

English abstract:
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

Related Projects:
Project Head Stefan Woltran:

Created from the Publication Database of the Vienna University of Technology.