2026-07-21T03:15:16Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:4910 2024-03-06T10:35:32Z ddc:004 open_access

Understanding Model Counting for beta-acyclic CNF-formulas Brault-Baron, Johann Capelli, Florent Mengel, Stefan model counting hypergraph acyclicity structural tractability 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Johann Brault-Baron and Florent Capelli and Stefan Mengel 2015 Is Part Of LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.STACS.2015.143 urn:nbn:de:0030-drops-49106 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.143 eng https://creativecommons.org/licenses/by/3.0/legalcode