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。我们的结果表明,图形演算为推理计数问题提供了一种直观且有用的框架。