Model counting for CNF formulas of bounded modular treewidth

Paulusma, D.; Slivovsky, S.; Szeider, S.

Abstract

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.

Citation

Paulusma, D., Slivovsky, S., & Szeider, S. (2016). Model counting for CNF formulas of bounded modular treewidth. Algorithmica, 76(1), 168-194. https://doi.org/10.1007/s00453-015-0030-x

• Journal Article Type: Article
• Acceptance Date: Jul 8, 2015
• Online Publication Date: Jul 17, 2015
• Publication Date: Sep 1, 2016
• Deposit Date: Aug 12, 2015
• Publicly Available Date: Jul 17, 2016
• Journal: Algorithmica
• Print ISSN: 0178-4617
• Electronic ISSN: 1432-0541
• Publisher: Springer
• Peer Reviewed: Peer Reviewed
• Volume: 76
• Issue: 1
• Pages: 168-194
• DOI: https://doi.org/10.1007/s00453-015-0030-x
• Keywords: Propositional Satisfiability, Model Counting, Algorithms.
• Public URL: https://durham-repository.worktribe.com/output/1424354