Understanding the complexity of #SAT using knowledge compilation

TL;DR

This paper explores the complexity of #SAT by comparing two main techniques, revealing that certain formulas are efficiently solvable by one method but not the other, thus clarifying their computational boundaries.

Contribution

It introduces a family of formulas that differentiate the efficiency of two #SAT solving techniques and links their complexity to boolean circuit representations.

Findings

Exhibits formulas solvable in polynomial time by exhaustive DPLL but not by structure-based methods.

Shows beta-acyclic formulas can be represented by polynomial size circuits for the first method.

Provides tools for algorithm design on beta-acyclic hypergraphs.

Abstract

Two main techniques have been used so far to solve the #P-hard problem #SAT. The first one, used in practice, is based on an extension of DPLL for model counting called exhaustive DPLL. The second approach, more theoretical, exploits the structure of the input to compute the number of satisfying assignments by usually using a dynamic programming scheme on a decomposition of the formula. In this paper, we make a first step toward the separation of these two techniques by exhibiting a family of formulas that can be solved in polynomial time with the first technique but needs an exponential time with the second one. We show this by observing that both techniques implicitely construct a very specific boolean circuit equivalent to the input formula. We then show that every beta-acyclic formula can be represented by a polynomial size circuit corresponding to the first method and exhibit a family of beta-acyclic formulas which cannot be represented by polynomial size circuits corresponding to the second method. This result shed a new light on the complexity of #SAT and related problems on beta-acyclic formulas. As a byproduct, we give new handy tools to design algorithms on beta-acyclic hypergraphs.