Better Algorithms for Satisfiability Problems for Formulas of Bounded Rank-width

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.