Note: [] Address for correspondence: Faculty of Informatics, Masaryk University, Botanická 68a, Brno, Czech Republic
Abstract: We provide a parameterized algorithm for the propositional model counting problem #SAT, the runtime of which has a single-exponential dependency on the rank-width of the signed graph of a formula. That is, our algorithm runs in time $\cal{O}(t^3 \cdot 2^{3t(t+1)/2} \cdot \vert\phi\vert)$ for a width-t rank-decomposition of the input φ, and can be of practical interest for small values of rank-width. Previously, analogical algorithms have been known – e.g. [Fischer, Makowsky, and Ravve] – with a single-exponential dependency on the clique-width k of the signed graph of a formula with a given k-expression. Our algorithm presents an exponential runtime improvement over the worst-case scenario of the previous one, since clique-width reaches up to exponentially higher values than rankwidth. We also provide an algorithm for the MAX-SAT problem along the same lines.
Keywords: propositional model counting, satisfiability, rank-width, clique-width, parameterized Complexity
