论文标题
张量网络重写策略以满足和计算
Tensor Network Rewriting Strategies for Satisfiability and Counting
论文作者
论文摘要
我们在同等基础上提供SAT和#SAT的图形处理。 #SAT的实例可以以标准方式表示为张量网络。这些张量网络是通过ZH-Calculus的图表来解释的：一个系统，以通过简单发电机构建的图表来推理张量超过C的系统，在该图中，仅通过图的转换，可以进行计算。通常，ZH图的节点在确定张量系数的C上采用参数。对于#SAT实例的标准表示形式，系数为0或1的值。然后，通过选择图表的系数以范围范围，我们代表SAT的相应实例。因此，通过解释布尔半度性或复数数字上的图表，我们可以实例化问题的决策或计数版本。我们发现，对于已知在P中已知的类，例如2SAT和#XORSAT，存在适当的重写规则可以有效地简化图表，从而在多项式时间内产生解决方案。相反，对于已知的NP完整类别的类，例如3SAT或＃p-Complete，例如＃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.
