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 formulas of bounded modular treewidth.

Paulusma, D. and Slivovsky, S. and Szeider, S. (2016) 'Model counting for CNF formulas of bounded modular treewidth.', Algorithmica., 76 (1). pp. 168-194.


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.

Item Type:Article
Keywords:Propositional Satisfiability, Model Counting, Algorithms.
Full text:(AM) Accepted Manuscript
Download PDF
Publisher Web site:
Publisher statement:The final publication is available at Springer via
Date accepted:08 July 2015
Date deposited:19 August 2015
Date of first online publication:17 July 2015
Date first made open access:17 July 2016

Save or Share this output

Look up in GoogleScholar