Understanding the complexity of #SAT using knowledge compilation
Understanding the complexity of #SAT using knowledge compilation
复制标题
了解复杂性
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Florent Capelli
中科院分区：
文献类型：
--
作者：
Florent Capelli
到目前为止，已经使用了两种主要技术来解决#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 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.