Parallel Weighted Model Counting with Tensor Networks

TL;DR

This paper explores the use of multi-core and GPU acceleration for tensor-network-based weighted model counting, demonstrating significant performance improvements over existing methods.

Contribution

It introduces parallel and GPU-accelerated tensor contraction techniques for weighted model counting, enhancing efficiency beyond prior single-core approaches.

Findings

Parallel portfolio of tree-decomposition solvers improves tensor contraction order

GPU-based tensor contractions using TensorFlow accelerate computations

Significant performance gains over previous single-core methods

Abstract

A promising new algebraic approach to weighted model counting makes use of tensor networks, following a reduction from weighted model counting to tensor-network contraction. Prior work has focused on analyzing the single-core performance of this approach, and demonstrated that it is an effective addition to the current portfolio of weighted-model-counting algorithms. In this work, we explore the impact of multi-core and GPU use on tensor-network contraction for weighted model counting. To leverage multiple cores, we implement a parallel portfolio of tree-decomposition solvers to find an order to contract tensors. To leverage a GPU, we use TensorFlow to perform the contractions. We compare the resulting weighted model counter on 1914 standard weighted model counting benchmarks and show that it significantly improves the virtual best solver.