Hypergraph Acyclicity and Propositional Model Counting

TL;DR

This paper identifies a new class of hypergraphs allowing polynomial-time solutions for #SAT, introduces an algorithm for their decomposition, and discusses the boundaries of tractability in propositional model counting.

Contribution

It establishes that #SAT is polynomial-time solvable for hypergraphs with disjoint branches decompositions and provides an algorithm to find such decompositions.

Findings

#SAT solvable in polynomial time for hypergraphs with disjoint branches decompositions

Algorithm to compute disjoint branches decomposition efficiently

Extensions of the class lead to intractability, indicating boundaries of the approach

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.