ABSTRACT. In this talk, we first give an overview on solving #SAT using parameterized algorithms that exploit small treewidth. The problem #SAT asks to output the number of solutions of a Boolean formula. If the treewidth of a graph representation of the given formula is fixed, one can solve #SAT efficiently by means of a dynamic programming algorithm on tree decompositions.

However, finding an optimal tree decomposition is itself an NP-hard problem. Existing methods for finding tree decompositions of small width either (a) yield optimal tree decompositions but are applicable only to small instances or (b) are based on greedy heuristics which often yield tree decompositions that are far from optimal. We propose a new method that combines (a) and (b), where a heuristically obtained tree decomposition is improved locally. We sketch results of an experimental evaluation of our new method.

Further, we present a novel architecture of dynamic programming for efficient parallel execution on the GPU. We provide thorough experiments and compare the runtime of our system with state-of-the-art solvers. Our results are encouraging if instances have treewidth at most 30, which is the case for the majority of counting benchmark instances.