Understanding model counting for $\beta$-acyclic CNF-formulas

TL;DR

This paper introduces a polynomial-time algorithm for counting solutions in $eta$-acyclic CNF formulas, using an elimination order approach, and provides evidence that dynamic programming methods may not be suitable for this class.

Contribution

It presents a novel polynomial-time algorithm for $eta$-acyclic $ ext{ ext{ ext#SAT}}$ that diverges from traditional dynamic programming techniques.

Findings

The algorithm works along an elimination order.

It solves a weighted version of constraint satisfaction.

Evidence suggests no standard dynamic programming algorithm exists for this class.

Abstract

We extend the knowledge about so-called structural restrictions of $\mathrm{\#SAT}$ by giving a polynomial time algorithm for $\beta$-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 $\beta$-acyclic $\mathrm{\#SAT}$.