Simulating Quantum Circuits by Model Counting

TL;DR

This paper introduces a novel approach to simulate universal quantum circuits efficiently using weighted model counting, leveraging stabilizer formalism and demonstrating empirical advantages over existing methods.

Contribution

It provides the first linear encoding of Clifford+T circuits for weighted model counting, enabling efficient classical simulation of quantum circuits.

Findings

Model counting often outperforms ZX calculus-based simulation.

The approach enables efficient simulation of universal quantum circuits.

Open-source implementation demonstrates practical viability.

Abstract

Quantum circuit compilation comprises many computationally hard reasoning tasks that nonetheless lie inside #$\mathbf{P}$ and its decision counterpart in $\mathbf{PP}$. The classical simulation of general quantum circuits is a core example. We show for the first time that a strong simulation of universal quantum circuits can be efficiently tackled through weighted model counting by providing a linear encoding of Clifford+T circuits. To achieve this, we exploit the stabilizer formalism by Knill, Gottesmann, and Aaronson and the fact that stabilizer states form a basis for density operators. With an open-source simulator implementation, we demonstrate empirically that model counting often outperforms state-of-the-art simulation techniques based on the ZX calculus and decision diagrams. Our work paves the way to apply the existing array of powerful classical reasoning tools to realize efficient quantum circuit compilation; one of the obstacles on the road towards quantum supremacy.