Skip to main content

Research Repository

Advanced Search

Model counting for CNF formulas of bounded modular treewidth

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

Model counting for CNF formulas of bounded modular treewidth Thumbnail


Authors

S. Slivovsky

S. Szeider



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

Files





You might also like



Downloadable Citations