Abstract Quantum circuit compilation comprises many computationally hard reasoning tasks that lie inside #
P P and its decision counterpart in
PP 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+Tcircuits. 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.
A decision diagram (DD) is a graph-like data structure for homomorphic compression of Boolean and pseudo-Boolean functions. Over the past decades, decision diagrams have been successfully applied to verification, linear algebra, stochastic reasoning, and quantum circuit analysis. Floating-point errors have, however, significantly slowed down practical implementations of real- and complex-valued decision diagrams. In the context of quantum computing, attempts to mitigate this numerical instability have thus far lacked theoretical scaling guarantees and have had only limited success in practice. Here, we focus on the analysis of quantum circuits consisting of Clifford gates and
T gates (a common universal gate set). We first hand-craft an algebraic representation for complex numbers, which replace the floating point coefficients in a decision diagram. Then, we prove that the sizes of these algebraic representations are linearly bounded in the number of
T gates and qubits, and constant in the number of Clifford gates. Furthermore, we prove that both the runtime and the number of nodes of decision diagrams are upper bounded as
2t⋅poly(g,n), where
t (
g) is the number of
t gates (Clifford gates) and
n the number of qubits. Our proofs are based on a
T-count dependent characterization of the density matrix entries of quantum states produced by circuits with Clifford+
T gates, and uncover a connection between a quantum state's stabilizer nullity and its decision diagram width. With an open source implementation, we demonstrate that our exact method resolves the inaccuracies occurring in floating-point-based counterparts and can outperform them due to lower node counts. Our contributions are, to the best of our knowledge, the first scaling guarantees on the runtime of (exact) quantum decision diagram simulation for a universal gate set.
Abstract Verifying equivalence between two quantum circuits is a hard problem, that is nonetheless crucial in compiling and optimizing quantum algorithms for real-world devices. This paper gives a Turing reduction of the (universal) quantum circuits equivalence problem to weighted model counting (WMC). Our starting point is a folklore theorem showing that equivalence checking of quantum circuits can be done in the so-called Pauli-basis. We combine this insight with a WMC encoding of quantum circuit simulation, which we extend with support for the Toffoli gate. Finally, we prove that the weights computed by the model counter indeed realize the reduction. With an open-source implementation, we demonstrate that this novel approach can outperform a state-of-the-art equivalence-checking tool based on ZX calculus and decision diagrams.
Abstract We introduce an enhanced technique for strong classical simulation of quantum circuits which combines the ‘sum-of-stabilisers’ method with an automated simplification strategy based on the ZX-calculus. Recently it was shown that quantum circuits can be classically simulated by expressing the non-stabiliser gates in a circuit as magic state injections and decomposing them in chunks of 2–6 states at a time, obtaining sums of (efficiently-simulable) stabiliser states with many fewer terms than the naive approach. We adapt these techniques from the original setting of Clifford circuits with magic state injection to generic ZX-diagrams and show that, by interleaving this ‘chunked’ decomposition with a ZX-calculus-based simplification strategy, we can obtain stabiliser decompositions that are many orders of magnitude smaller than existing approaches. We illustrate this technique to perform exact norm calculations (and hence strong simulation) on the outputs of random 50- and 100-qubit Clifford + T circuits with up to 70 T-gates as well as a family of hidden shift circuits previously considered by Bravyi and Gosset with over 1000 T-gates.
We study classical simulation of quantum computation, taking the Gottesman-Knill theorem as a starting point. We show how each Clifford circuit can be reduced to an equivalent, manifestly simulatable circuit (normal form). This provides a simple proof of the Gottesman-Knill theorem without resorting to stabilizer techniques. The normal form highlights why Clifford circuits have such limited computational power in spite of their high entangling power. At the same time, the normal form shows how the classical simulation of Clifford circuits fits into the standard way of embedding classical computation into the quantum circuit model. This leads to simple extensions of Clifford circuits which are classically simulatable. These circuits can be efficiently simulated by classical sampling (``weak simulation'') even though the problem of exactly computing the outcomes of measurements for these circuits (``strong simulation'') is proved to be
#P-complete---thus showing that there is a separation between weak and strong classical simulation of quantum computation.
Strongly simulating a quantum circuit, that is, computing an output amplitude, can be done by summing the circuit's Feynman paths: a weighted count over assignments to Boolean path variables. The circuit's gates induce correlations among these variables, forming a graph whose structure controls several exact simulation routes. This sum-of-powers (SOP) viewpoint underlies recent simulators built on binary decision diagrams and weighted model counting.
For a quadratic SOP with
n variables, even modulus
r, and a rank-decomposition of its variable graph of width
k, our dynamic program (DP) computes an amplitude using only
O(4kpoly(n)) arithmetic operations. For Clifford
+T circuits, the amplitude is given by an SOP with modulus
8.
Rank-width never exceeds linear rank-width, which governs some decision-diagram approaches, and is at most one greater than the Markov--Shi contraction complexity of the circuit tensor network. Moreover, there are non-Clifford families of bounded rank-width where both competing parameters diverge. We also present a stabilizer-rank optimization, exploiting that the DP tables are stabilizer-type Gauss sums. Each subtree runs at the width price of its cut-ranks or at a magic price that discharges the non-Clifford phases below it. The resulting best total cost never exceeds
O(4kpoly(n)), yet is polynomial on mixed families where the pure rank-width and pure
T-count guarantees are both exponential. Clifford amplitudes take polynomial time on any graph, the exact-amplitude consequence of Gottesman--Knill.
A prototype evaluation on standard circuit benchmarks finds treewidth bucket elimination the strongest baseline, with the new rank-width DP complementary: it wins on structured families where treewidth blows up.