Understanding model counting for $β$-acyclic CNF-formulas
This work addresses the computational complexity of #SAT for researchers in theoretical computer science, offering a novel algorithmic approach for a specific structural class.
The paper tackles the problem of model counting for β-acyclic CNF formulas by presenting a polynomial-time algorithm that uses an elimination order and weighted constraint solving, deviating from dynamic programming approaches, and provides evidence that dynamic programming may not be feasible for this case.
We extend the knowledge about so-called structural restrictions of $\mathrm{\#SAT}$ by giving a polynomial time algorithm for $β$-acyclic $\mathrm{\#SAT}$. In contrast to previous algorithms in the area, our algorithm does not proceed by dynamic programming but works along an elimination order, solving a weighted version of constraint satisfaction. Moreover, we give evidence that this deviation from more standard algorithm is not a coincidence, but that there is likely no dynamic programming algorithm of the usual style for $β$-acyclic $\mathrm{\#SAT}$.