一句话：通过电路表示分离 #SAT 的两类求解技术，揭示 β-acyclic 公式的复杂度。
论文关注 #SAT 的复杂度，比较两类主要求解技术：一是实践中基于 DPLL 扩展的 exhaustive DPLL，二是理论上利用公式结构、在分解上动态规划的方法。作者指出二者都隐式构造与输入公式等价的特定布尔电路，从而可通过电路表示来分离两种技术：展示一族公式在第一类方法下可多项式时间求解，但第二类方法需要指数时间。进一步证明每个 β-acyclic 公式都可由第一类方法对应的多项式大小电路表示，并给出无法由第二类方法对应的多项式大小电路表示的 β-acyclic 公式族。该结果揭示了 β-acyclic 公式上 #SAT 及相关问题的复杂度，并附带提供了设计 β-acyclic 超图算法的新工具。
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 implicitly construct a very specific Boolean circuit equivalent to the input formula. We then show that every β-acyclic formula can be represented by a polynomial size circuit corresponding to the first method and exhibit a family of β-acyclic formulas which cannot be represented by polynomial size circuits corresponding to the second method. This result sheds a new light on the complexity of #SAT and related problems on β-acyclic formulas. As a byproduct, we give new handy tools to design algorithms on β-acyclic hypergraphs.