License: Creative Commons Attribution-NoDerivs 3.0 Unported license (CC BY-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2013.55
URN: urn:nbn:de:0030-drops-39226
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/3922/
Go to the corresponding LIPIcs Volume Portal

Paulusma, Daniel ; Slivovsky, Friedrich ; Szeider, Stefan

Model Counting for CNF Formulas of Bounded Modular Treewidth

pdf-format:
10.pdf (0.6 MB)

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.

BibTeX - Entry

@InProceedings{paulusma_et_al:LIPIcs:2013:3922,
  author =	{Daniel Paulusma and Friedrich Slivovsky and Stefan Szeider},
  title =	{{Model Counting for CNF Formulas of Bounded Modular Treewidth}},
  booktitle =	{30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)},
  pages =	{55--66},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-50-7},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{20},
  editor =	{Natacha Portier and Thomas Wilke},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/3922},
  URN =		{urn:nbn:de:0030-drops-39226},
  doi =		{10.4230/LIPIcs.STACS.2013.55},
  annote =	{Keywords: Satisfiability, Model Counting, Parameterized Complexity}
}

Keywords: Satisfiability, Model Counting, Parameterized Complexity
Collection: 30th International Symposium on Theoretical Aspects of Computer Science (STACS 2013)
Issue Date: 2013
Date of publication: 26.02.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI