Counting the solutions to Boolean formulae defines the problem #SAT, which is complete for the complexity class #P. We use the ZH-calculus, a universal and complete graphical language for linear maps which naturally encodes counting problems in terms of diagrams, to give graphical reductions from #SAT to several related counting problems. Some of these graphical reductions, like to #2SAT, are substantially simpler than known reductions via the matrix permanent. Additionally, our approach allows us to consider the case of counting solutions modulo an integer on equal footing. Finally, since the ZH-calculus was originally introduced to reason about quantum computing, we show that the problem of evaluating ZH-diagrams in the fragment corresponding to the Clifford+T gateset, is in $FP^{\#P}$. Our results show that graphical calculi represent an intuitive and useful framework for reasoning about counting problems.
翻译:布尔公式解的计数问题定义了#SAT,该问题是复杂度类#P的完全问题。我们使用ZH演算——一种通用且完备的线性映射图形语言,通过图解自然编码计数问题——给出从#SAT到若干相关计数问题的图形归约。其中部分图形归约(如到#2SAT的归约)比已知的通过矩阵积和式进行的归约更简洁。此外,我们的方法能够统一处理模整数解计数问题。最后,由于ZH演算最初是为量子计算推理而引入,我们证明:对应于Clifford+T量子门集的ZH图计算问题属于$FP^{\#P}$。研究结果表明,图解演算为推理计数问题提供了直观且实用的框架。