Hypergraph acyclicity and propositional model counting
From MaRDI portal
Abstract: We show that the propositional model counting problem #SAT for CNF- formulas with hypergraphs that allow a disjoint branches decomposition can be solved in polynomial time. We show that this class of hypergraphs is incomparable to hypergraphs of bounded incidence cliquewidth which were the biggest class of hypergraphs for which #SAT was known to be solvable in polynomial time so far. Furthermore, we present a polynomial time algorithm that computes a disjoint branches decomposition of a given hypergraph if it exists and rejects otherwise. Finally, we show that some slight extensions of the class of hypergraphs with disjoint branches decompositions lead to intractable #SAT, leaving open how to generalize the counting result of this paper.
Recommendations
Cited in
(7)- Tractability beyond -acyclicity for conjunctive queries with negation and SAT
- On freedom and independence in hypergraphs of models of theories
- Understanding model counting for -acyclic CNF-formulas
- scientific article; zbMATH DE number 638367 (Why is no real title available?)
- scientific article; zbMATH DE number 1756016 (Why is no real title available?)
- Understanding the complexity of \#SAT using knowledge compilation
- scientific article; zbMATH DE number 6739879 (Why is no real title available?)
This page was built for publication: Hypergraph acyclicity and propositional model counting
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192085)