Tensor Network Algorithms for Counting 2-SAT Solutions

We present a tensor network method for counting the number of solutions of 2-SAT problems (#2-SAT). We embed 2-SAT problems into a two dimensional square lattice network, and we encode the number of solutions in a tensor trace, which we compute by gradually contracting the tensor network. To optimize the contraction, we use a compression-decimation algorithm to propagate local constraints to longer range before coarse-graining the tensor network. Iterations of these steps allows the network to collapse gradually while containing the tensor dimensions. We compare the results and performance of our tensor-based algorithm with those from the sharpSAT solver based on the DPLL algorithm.