论文标题
图形#SAT算法，用于具有小子句密度的公式
A Graphical #SAT Algorithm for Formulae with Small Clause Density
论文作者
论文摘要
我们使用ZH-Calculus研究了布尔值的可满足性问题的计数版本，这是一种最初引入的图形语言，该语言最初是为了理论量子电路的理由。使用此功能，我们将#SAT推广到我们称为＃SAT+ - 的加权变体，这对于类Gapp是完整的。我们表明，与以前从#sat降低到＃2SAT的有效线性时间缩短到＃2SAT+ - ，它通过多项式因子炸毁了公式的大小。我们的主要概念贡献是将权重引入#SAT可以进行更有效的翻译，我们使用它来消除对从句宽度k的依赖性，在这种情况下。我们观察到，＃2SAT的DPLL风格算法可以直接适用于＃2SAT+ - 因此，适用＃2SAT的最著名上限。就变量应用＃2SAT的上限为我们提供了#SAT的上限，就条款和变量而言，对于m/n <2.25的小节密度优于o*（2^n），并改善了先前的平均案例和最差案例和最差的k> = 6和k> = 4。在条款上应用类似的界限会在公式的长度上产生O*（1.1740^l）的界限。据我们所知，这些是独立于子句大小和公式长度的第一个非平凡的上限。基于Kutzkov的结果，我们发现1.2577 <m/n <= 7/3的＃3SAT上有一个改进的绑定。最后，我们使用这种技术来根据大门总数来找到计算量子电路振幅的复杂性的上限。我们的结果表明，图形推理可以导致新的算法见解，即使是在量子计算的范围之外，该量子计算的范围也是如此。
We study the counting version of the Boolean satisfiability problem #SAT using the ZH-calculus, a graphical language originally introduced to reason about quantum circuits. Using this, we generalize #SAT to a weighted variant we call #SAT+-, which is complete for the class GapP. We show there is an efficient linear-time reduction from #SAT to #2SAT+-, unlike previous reductions from #SAT to #2SAT which blow up the size of the formula by a polynomial factor. Our main conceptual contribution is that introducing weights to #SAT allows for more efficient translations, and we use this to remove the dependence on clause width k in this case. We observe that DPLL-style algorithms for #2SAT can be adapted to #2SAT+- directly and hence the best-known upper bounds for #2SAT apply. Applying an upper bound for #2SAT in terms of variables gives us upper bounds for #SAT in terms of clauses and variables that are better than O*(2^n) for small clause densities of m/n < 2.25, and improve on previous average-case and worst-case bounds for k >= 6 and k >= 4, respectively. Applying a similar bound in terms of clauses produces a bound of O*(1.1740^L) in terms of the length of the formula. These are, to our knowledge, the first non-trivial upper bounds for #SAT that is independent of clause size, and in terms of formula length, respectively. Based on a result of Kutzkov, we find an improved bound on #3SAT for 1.2577 < m/n <= 7/3. Finally, we use this technique to find an upper bound on the complexity of calculating amplitudes of quantum circuits in terms of the total number of gates. Our results demonstrate that graphical reasoning can lead to new algorithmic insights, even outside the domain of quantum computing that the calculus was intended for.
