# Tensor Network Contractions for #SAT

arXiv: https://arxiv.org/abs/1405.7375 · HTML: https://mlsanity.com/paper/1405.7375/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 28 May 2014.

## Built on by (most cited first, 2 of 2)

- [Equivariant Polynomials for Graph Neural Networks](https://mlsanity.com/paper/2302.11556/) (2023)
- [Cons-training Tensor Networks: Embedding and Optimization Over Discrete Linear Constraints](https://mlsanity.com/paper/2405.09005/) (2024)

## Abstract (arXiv)

The computational cost of counting the number of solutions satisfying a Boolean formula, which is a problem instance of #SAT, has proven subtle to quantify. Even when finding individual satisfying solutions is computationally easy (e.g. 2-SAT, which is in P), determining the number of solutions is #P-hard. Recently, computational methods simulating quantum systems experienced advancements due to the development of tensor network algorithms and associated quantum physics-inspired techniques. By these methods, we give an algorithm using an axiomatic tensor contraction language for n-variable #SAT instances with complexity O((g+cd)O(1) 2c) where c is the number of COPY-tensors, g is the number of gates, and d is the maximal degree of any COPY-tensor. Thus, counting problems can be solved efficiently when their tensor network expression has at most O(log c) COPY-tensors and polynomial fan-out. This framework also admits an intuitive proof of a variant of the Tovey conjecture (the r,1-SAT instance of the Dubois-Tovey theorem). This study increases the theory, expressiveness and application of tensor based algorithmic tools and provides an alternative insight on these problems which have a long history in statistical physics and computer science.