Skip to main content

Research Repository

Advanced Search

Model counting for CNF formuals of bounded module treewidth

Paulusma, D.; Slivovksy, F.; Szeider, S.

Model counting for CNF formuals of bounded module treewidth Thumbnail


Authors

F. Slivovksy

S. Szeider



Contributors

Natacha Portier
Editor

Thomas Wilke
Editor

Abstract

The modular treewidth of a graph is its treewidth after the contraction of modules. Modular treewidth properly generalizes treewidth and is itself properly generalized by clique-width. We show that the number of satisfying assignments of a CNF formula whose incidence graph has bounded modular treewidth can be computed in polynomial time. This provides new tractable classes of formulas for which #SAT is polynomial. In particular, 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 time bound of our algorithm depends on the modular treewidth. We show that this dependency cannot be avoided subject to an assumption from Parameterized Complexity.

Citation

Paulusma, D., Slivovksy, F., & Szeider, S. (2013). Model counting for CNF formuals of bounded module treewidth. In N. Portier, & T. Wilke (Eds.), 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013) (55-66). https://doi.org/10.4230/lipics.stacs.2013.55

Conference Name 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)
Conference Location Kiel, Christian-Albrechts-Universität zu Kiel, Germany
Publication Date Jan 1, 2013
Deposit Date Mar 11, 2013
Publicly Available Date Mar 29, 2024
Pages 55-66
Series Title Leibniz International Proceedings in Informatics (LIPIcs)
Series Number 20
Series ISSN 1868-8969
Book Title 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013).
ISBN 9783939897507
DOI https://doi.org/10.4230/lipics.stacs.2013.55
Keywords Satisfiability, Model Counting, Parameterized Complexity.
Public URL https://durham-repository.worktribe.com/output/1156230
Additional Information Conference dates: Feb 27–Mar 2, 2013

Files





You might also like



Downloadable Citations