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
URL: https://drops.dagstuhl.de/opus/volltexte/2015/4910/
Brault-Baron, Johann ; Capelli, Florent ; Mengel, Stefan
Understanding Model Counting for beta-acyclic CNF-formulas
| pdf-format: |
|
Abstract
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
@InProceedings{braultbaron_et_al:LIPIcs:2015:4910,
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 = {http://drops.dagstuhl.de/opus/volltexte/2015/4910},
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 | |
| Seminar: | 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015) | |
| Issue date: | 2015 | |
| Date of publication: | 26.02.2015 |
