可满足性和计数的张量网络重写策略
Tensor Network Rewriting Strategies for Satisfiability and Counting
摘要：
我们平等地提供了SAT和#SAT的图形处理。#SAT的网络可以以标准的方式表示为张量网络。这些张量网络可以用ZH演算的图来解释：这是一个用简单生成器构建的图来推理C上张量的系统，其中计算可以单独通过图的变换来进行。一般来说，ZH图的节点接受C上的参数，这些参数决定了张量系数;对于#SAT实例的标准表示，系数取值为0或1。然后，通过选择一个图的系数在B上的范围，我们表示SAT的相应实例。因此，通过在布尔半环或复数上解释图，我们实例化了问题的决策或计数版本。我们发现，对于类已知是在P，如2SAT和#XORSAT，存在适当的重写规则允许有效的简化图，产生解决方案在多项式时间。相比之下，对于已知为NP完全的类，例如3SAT，或#P完全的类，例如#2SAT，相应的重写规则在图中引入超边，其数量不容易由多项式限制。这种图解方法统一了CSP和#CSP的复杂性诊断，并显示出有助于基于张量网络收缩的算法的希望。
英文摘要：
We provide a graphical treatment of SAT and #SAT on equal footing. Instances of #SAT can be represented as tensor networks in a standard way. These tensor networks are interpreted by diagrams of the ZH-calculus: a system to reason about tensors over C in terms of diagrams built from simple generators, in which computation may be carried out by transformations of diagrams alone. In general, nodes of ZH diagrams take parameters over C which determine the tensor coefficients; for the standard representation of #SAT instances, the coefficients take the value 0 or 1. Then, by choosing the coefficients of a diagram to range over B, we represent the corresponding instance of SAT. Thus, by interpreting a diagram either over the boolean semiring or the complex numbers, we instantiate either the decision or counting version of the problem. We find that for classes known to be in P, such as 2SAT and #XORSAT, the existence of appropriate rewrite rules allows for efficient simplification of the diagram, producing the solution in polynomial time. In contrast, for classes known to be NP-complete, such as 3SAT, or #P-complete, such as #2SAT, the corresponding rewrite rules introduce hyperedges to the diagrams, in numbers which are not easily bounded above by a polynomial. This diagrammatic approach unifies the diagnosis of the complexity of CSPs and #CSPs and shows promise in aiding tensor network contraction-based algorithms.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
