Model Counting for CNF Formulas of Bounded Modular Treewidth
Symposium on Theoretical Aspects of Computer Science(2015)
摘要
We define the modular treewidth of a graph as its treewidth after contraction of modules. This parameter properly generalizes treewidth and is itself properly generalized by clique-width. We show that the number of satisfying assignments can be computed in polynomial time for CNF formulas whose incidence graphs have bounded modular treewidth. Our result generalizes known results for the treewidth of incidence graphs and is incomparable with known results for clique-width (or rank-width) of signed incidence graphs. The contraction of modules is an effective data reduction procedure. Our algorithm is the first one to harness this technique for #SAT. The order of the polynomial bounding the runtime of our algorithm depends on the modular treewidth of the input formula. We show that it is unlikely that this dependency can be avoided by proving that SAT is W[1]-hard when parameterized by the modular incidence treewidth of the given CNF formula.
更多查看译文
关键词
Propositional Satisfiability,Model Counting,Algorithms
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络