LIPIcs.STACS.2015.143.pdf
- Filesize: 0.59 MB
- 14 pages
Document
Understanding Model Counting for beta-acyclic CNF-formulas
Authors
-
Part of:
Volume:
32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: Symposium on Theoretical Aspects of Computer Science (STACS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-02-26
Cite AsGet BibTex
Johann Brault-Baron, Florent Capelli, and Stefan Mengel. Understanding Model Counting for beta-acyclic CNF-formulas. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 143-156, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.STACS.2015.143
https://doi.org/10.4230/LIPIcs.STACS.2015.143
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.
Keywords
- model counting
- hypergraph acyclicity
- structural tractability
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads