We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.

Durham Research Online
You are in:

Model counting for CNF formuals of bounded module treewidth.

Paulusma, Daniel and Slivovksy, F. and Szeider, S. (2013) 'Model counting for CNF formuals of bounded module treewidth.', in 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013). Saarbrücken, Germany: Schloss Dagstuh, pp. 55-66. Leibniz International Proceedings in Informatics (LIPIcs). (20).


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.

Item Type:Book chapter
Additional Information:The 30th Symposium on Theoretical Aspects of Computer Science was held in Kiel, at Christian-Albrechts-Universität zu Kiel, 27 Feb 27 - 2 Mar, 2013.
Keywords:Satisfiability, Model Counting, Parameterized Complexity.
Full text:(VoR) Version of Record
Available under License - Creative Commons Attribution No Derivatives.
Download PDF
Publisher Web site:
Publisher statement:This article is available under a CC-BY-ND licence. See
Date accepted:No date available
Date deposited:08 January 2015
Date of first online publication:2013
Date first made open access:No date available

Save or Share this output

Look up in GoogleScholar