Simulating Quantum Circuits by Model Counting
Jingyi Mei, Marcello Bonsangue, Alfons Laarman
TL;DR
The paper tackles the problem of strong classical simulation of universal quantum circuits and shows that strong simulation can be efficiently achieved via a weighted model counting encoding with linear size $O(n+m)$ for Clifford+$T$ circuits. It leverages the stabilizer formalism to express density operators in the stabilizer basis, avoiding complex amplitudes and permitting negative weights in weighted model counting. An open-source tool, QCMC, implements this encoding atop the GPMC engine, and empirical benchmarks demonstrate that the approach often outperforms ZX-calculus–based QuiZX and CFLOBDD–based Quasimodo on random Clifford+$T$ circuits and MQT Bench algorithms, with notable memory advantages. This framework broadens the applicability of classical reasoning tools to quantum circuit compilation and extends to rotation gates beyond Clifford+$T$, offering a flexible path toward practical quantum circuit analysis and addressing obstacles on the road to quantum supremacy.
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.