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) ( 2 3 k + 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+n2log2(n)) 4 k ( n + n 2  log 2 ( 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 G1 G 1 and G2 G 2 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 (12) (2001) 2352].
tree-width clique-width satisfiability (sat) counting problems fixed parameter tractable (fpt)