Counting truth assignments of formulas of bounded tree-width or clique-width

We study algorithms for ♯SAT♯SAT and its generalized version ♯GENSAT♯GENSAT, the problem of computing the number of satisfying assignments of a set of propositional clauses ΣΣ. For this purpose we consider the clauses given by their incidence graph, a signed bipartite graph SI(Σ)SI(Σ), and its derived graphs I(Σ)I(Σ) and P(Σ)P(Σ).It is well known, that, given a graph of tree-width k, a k-tree decomposition can be found in polynomial time. Very recently Oum and Seymour have shown that, given a graph of clique-width k  , a (23k+2-1)(23k+2-1)-parse tree witnessing clique-width can be found in polynomial time.In this paper we present an algorithm for ♯GENSAT♯GENSAT for formulas of bounded tree-width k   which runs in time 4k(n+n2·log2(n))4k(n+n2·log2(n)), where n   is the size of the input. The main ingredient of the algorithm is a splitting formula for the number of satisfying assignments for a set of clauses ΣΣ where the incidence graph I(Σ)I(Σ) is a union of two graphs G1G1 and G2G2 with a shared induced subgraph H of size at most k. We also present analogue improvements for algorithms for formulas of bounded clique-width which are given together with their derivation.This considerably improves results for ♯SAT♯SAT, and hence also for SAT, previously obtained by Courcelle et al. [On the fixed parameter complexity of graph enumeration problems definable in monadic second order logic, Discrete Appl. Math. 108 (1–2) (2001) 23–52].