# Tensor Network Rewriting Strategies for Satisfiability and Counting

*Niel de Beaudrap‚ Aleks Kissinger and Konstantinos Meichanetzidis*

### Abstract

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 **ℂ** 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 **ℂ** 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 𝔹, 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.