License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.STACS.2015.143
URN: urn:nbn:de:0030-drops-49106
Go to the corresponding LIPIcs Volume Portal

Brault-Baron, Johann ; Capelli, Florent ; Mengel, Stefan

Understanding Model Counting for beta-acyclic CNF-formulas

10.pdf (0.6 MB)


We show that SAT on beta-acyclic CNF-formulas can be solved in polynomial time. In contrast to previous algorithms for other structurally restricted classes of formulas, our algorithm does not proceed by dynamic programming. Instead, it works along an elimination order, solving a weighted version of constraint satisfaction. We give evidence that this deviation from more standard algorithms is no coincidence by showing that it is outside of the framework recently proposed by Saether et al. (SAT 2014) which subsumes all other structural tractability results for #SAT known so far.

BibTeX - Entry

  author =	{Johann Brault-Baron and Florent Capelli and Stefan Mengel},
  title =	{{Understanding Model Counting for beta-acyclic CNF-formulas}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{143--156},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Ernst W. Mayr and Nicolas Ollinger},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{},
  URN =		{urn:nbn:de:0030-drops-49106},
  doi =		{10.4230/LIPIcs.STACS.2015.143},
  annote =	{Keywords: model counting, hypergraph acyclicity, structural tractability}

Keywords: model counting, hypergraph acyclicity, structural tractability
Collection: 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)
Issue Date: 2015
Date of publication: 26.02.2015

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