使用知识编译了解# SAT的复杂性
Understanding the complexity of #SAT using knowledge compilation
摘要：
到目前为止，已经使用了两种主要技术来解决#P-hard问题#SAT。第一个，在实践中使用，是基于扩展的DPLL的模型计数称为穷举DPLL。第二种方法，更多的理论，利用输入的结构来计算满意的分配的数量，通常使用一个动态规划计划的公式的分解。在本文中，我们对这两种技术的分离，展示了一个家庭的公式，可以解决在多项式时间的第一种技术，但需要一个指数的时间与第二个。我们通过观察这两种技术隐式地构建一个非常具体的布尔电路等效于输入公式。然后，我们表明，每一个β-非循环公式可以表示为一个多项式大小的电路对应的第一种方法，并表现出一个家庭的β-非循环公式，不能表示为多项式大小的电路对应的第二种方法。这一结果揭示了一个新的光的复杂性#SAT和相关问题的β-无环公式。作为一个副产品，我们提供了新的方便的工具来设计算法的β-无圈超图。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
