期刊
DISCRETE APPLIED MATHEMATICS
卷 156, 期 4, 页码 511-529出版社
ELSEVIER
DOI: 10.1016/j.dam.2006.06.020
关键词
satisfiability (SAT); counting problems; fixed parameter tractable (FPT); tree-width; clique-width
We study algorithms for #SAT and its generalized version #GENSAT, the problem of computing the number of satisfying assignments of a set of propositional clauses Sigma. For this purpose we consider the clauses given by their incidence graph, a signed bipartite graph SI(Sigma), and its derived graphs I (Sigma) and P (Sigma). 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 (2(3k+2)-1)-parse tree witnessing clique-width can be found in polynomial time. In this paper we present an algorithm for #GENSAT for formulas of bounded tree-width k which runs in time 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 Sigma where the incidence graph I (Sigma) is a union of two graphs G(1) and 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, 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]. (C) 2007 Elsevier B.V. All rights reserved.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据