TY - JOUR

T1 - Tensor Network Contractions for #SAT

AU - Biamonte, Jacob D.

AU - Morton, Jason

AU - Turner, Jacob

N1 - Funding Information:
We thank Tobias Fritz and Eduardo Mucciolo for providing feedback. JDB acknowledges financial support from the Fondazione Compagnia di San Paolo through the Q-ARACNE project and the Foundational Questions Institute (FQXi, under Grant FQXi-RFP3-1322). JM and JT acknowledges the NSF (under Grant NSF-1007808) for financial support.
Publisher Copyright:
© 2015, Springer Science+Business Media New York.

PY - 2015/9/1

Y1 - 2015/9/1

N2 - 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 $$\mathsf{{P}}$$P), determining the number of solutions can be #$$\mathsf{{P}}$$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)} 2^c)$$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, n-variable counting problems can be solved efficiently when their tensor network expression has at most $$O(\log n)$$O(logn) 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.

AB - 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 $$\mathsf{{P}}$$P), determining the number of solutions can be #$$\mathsf{{P}}$$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)} 2^c)$$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, n-variable counting problems can be solved efficiently when their tensor network expression has at most $$O(\log n)$$O(logn) 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.

UR - http://www.scopus.com/inward/record.url?scp=84938424019&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84938424019&partnerID=8YFLogxK

U2 - 10.1007/s10955-015-1276-z

DO - 10.1007/s10955-015-1276-z

M3 - Article

AN - SCOPUS:84938424019

SN - 0022-4715

VL - 160

SP - 1389

EP - 1404

JO - Journal of Statistical Physics

JF - Journal of Statistical Physics

IS - 5

ER -