Understanding model counting for beta-acyclic CNF-formulas

VCLA and WPI hosted a talk by Stefan Mengel on October 8, 2014.

ABSTRACT

Proposition model counting (#SAT) is the problem of counting satisfying assignments (models) to CNF-formulas. It is the canonical #P-hard counting problem and is important due to its applications in Artificial Intelligence. There is a growing body of work that successfully applies so-called structural restrictions to #SAT, i.e., restrictions to graphs and hypergraphs associated to CNF-Formulas to isolate tractable classes of instances. In this talk I will give an introduction into the area and discuss the case of beta-acyclic CNF-formulas. This class was only very recently shown to allow tractable model counting and interestingly the algorithm is very different from algorithms for other known tractable classes of formulas. I will give evidence that this deviation from more standard algorithms is no coincidence because beta-acyclic formulas lie outside of the framework recently proposed by Saether et al. (SAT 2014) which subsumes all other structural tractability results for #SAT known so far. The results presented in this talk are joint work with Johann Brault-Baron, and Florent Capelli.