Simulating Quantum Circuits by Model Counting

Quantum circuit compilation comprises many computationally hard reasoning tasks that lie inside #P and its decision counterpart in PP. The classical simulation of universal 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-length encoding of Clifford+T circuits. To achieve this, we exploit the stabilizer formalism by Knill, Gottesmann, and Aaronson by reinterpreting quantum states as a linear combination of stabilizer states. 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.