figure a
figure b

1 Introduction

Canonical, symbolic representations of Boolean functions—for example, Binary Decision Diagrams (BDDs) [5]—have a long history in automated system design and verification. More recently, such data-structures have found exciting new applications in quantum simulation. Quantum computers can theoretically solve certain problems much faster than traditional computers, but current quantum computers are error-prone and access to them is limited. The simulation of quantum algorithms on classical machines allows researchers to experiment with quantum algorithms even without access to reliable hardware.

Symbolic function representations are helpful in quantum simulation because a quantum system’s state can be viewed as a distribution over an exponential-sized set of basis-vectors (each representing a “classical” state). Such a state, as well as transformations that quantum algorithms typically apply to them, can often be efficiently represented using a symbolic data-structure. Simulating an algorithm then amounts to performing a sequence of symbolic operations.

Currently, there are a small number of open-source software systems that support such symbolic quantum simulation [1, 6, 8, 13, 16]. However, the underlying symbolic data-structure can have an enormous effect on simulation performance. In this tool paper, we present Quasimodo,Footnote 1 an extensible framework for symbolic quantum simulation. Quasimodo is specifically designed for easy extensibility to other backends to make it possible to experiment with a variety of symbolic data-structures. Quasimodo currently supports (i) BDDs [3, 5, 7], (ii) a weighted variant of BDDs [9, 14, 19, Ch. 5], and (iii) Context-Free-Language Ordered Binary Decision Diagrams CFLOBDDs [11], a recent canonical representation of Boolean functions that has been shown to outperform BDDs in many quantum-simulation tasks. Quasimodo also has a clean interface that formal-methods researchers can use to plug in new symbolic data-structures, which helps to lower the barrier to entry for formal-methods researchers interested in this area.

Users access Quasimodo through a Python interface. They can define a quantum algorithm as a quantum circuit using 18 different kinds of quantum gates, such as Hadamard, CNOT, and Toffoli gates. They can simulate the algorithm using a symbolic data-structure of their own choosing. Users can sample outcomes from the probability distribution computed through simulation, and can query the simulator for the probability of a specific outcome of a quantum computation over a set of quantum bits (qubits). The system also allows for a form of correctness checking: users are allowed to ask for the set of all high-probability outcomes and to check that these satisfy a given assertion.

Along with Quasimodo, we are releasing a suite of 7 established quantum algorithms encoded in the input language of Quasimodo. We hope that these algorithms will serve as benchmarks for future research on symbolic simulation and verification of quantum algorithms.

Organization. Section 2 gives an overview of quantum simulation. Section 3 gives a user-level overview of Quasimodo. Section 4 provides background on the symbolic data-structures available in Quasimodo. Section 5 describes the programming model of Quasimodo, and presents experimental results. Section 6 concludes.

2 Background on Quantum Simulation

Quantum algorithms on quantum computers can achieve polynomial to exponential speed-ups over classical algorithms on specific problems. However, because so far there are no practical scalable quantum computers, simulation of quantum circuits on classical computers can help in understanding how quantum algorithms work and scale. A simulation of a quantum-circuit computation [1, 6, 8, 11, 13, 19] uses a representation qs of a quantum state and performs operations on qs that correspond to quantum-circuit operations (gate applications and measurements on qs).

Simulating a quantum circuit can have advantages compared to executing the circuit on a quantum computer. For instance, some quantum algorithms perform multiple iterations of a particular quantum operator \({\textit{Op}}\) (e.g., k iterations, where \(k = 2^j\)). A simulation can operate on \({\textit{Op}}\) itself [19, Ch. 6], using j iterations of repeated squaring to create matrices for \({\textit{Op}}^2\), \({\textit{Op}}^4, \ldots \), \({\textit{Op}}^{2^j} = {\textit{Op}}^k\). In contrast, a physical device must apply \({\textit{Op}}\) sequentially, and thus performs \({\textit{Op}}\) \(k = 2^j\) times.

Many quantum algorithms require multiple measurements on the final state. After a measurement on a quantum computer, the quantum state collapses to the measured state. Thus, every successive measurement requires re-running the quantum circuit. However, with a simulation, the quantum state can be preserved across measurements, and thus the quantum circuit need only be executed once.

Fig. 1.
figure 1

An example of a Quasimodo program that performs a quantum-circuit computation in which the final quantum state is a GHZ state with 4,096 qubits. The program verifies that a measurement of the final quantum state has a 50% chance of returning the all-ones basis-state.

Full size image

3 Quasimodo’s Programming and Analysis Interface

This section presents an overview of Quasimodo from the perspective of a user of the Python API. A user can define a quantum-circuit computation and check the properties of the quantum state at various points in the computation. This section also explains how Quasimodo can be easily extended to include custom representations of the quantum state.

Example. Figure 1 shows an example of a quantum-circuit computation written using the Quasimodo API. To use the Quasimodo library, one needs to import the package, as shown in line 1. A user can then create a program that implements a quantum-circuit computation by

  • Initializing the quantum state by making a call to \(\texttt{QuantumState}\) with an argument that selects the desired backend data-structure and the number of qubits in the quantum state. (See line 7.) The example in Fig. 1 uses CFLOBDD as the backend simulator, but other data-structures can be used by changing the backend parameter to BDD or WBDD. \(\texttt{QuantumState}\) sets the initial quantum state to the all-zeros basis-state.

  • Applying single-qubit gates to the quantum state, such as Hadamard (h), Pauli-X (x), T-Gate (t), and others. The qubit to which they are to be applied is specified by passing the qubit number. (See line 8.)

  • Applying multi-qubit gates to the quantum state, such as CNOT (cx), Toffoli (ccx), SWAP (swap), and others. The qubits to which they are to be applied is specified by passing the qubit numbers. (See line 10.)

Note that queries on the quantum state do not have to be made only at the end of the program; they can also be interspersed throughout the circuit-simulation computation.

Quasimodo allows different backend data-structures to be used for representing quantum states. It comes with BDDs [3, 5, 7], a weighted variant of BDDs [9, 14, 19, Ch. 5], and CFLOBDDs [\(\{0, 1\}\), which defines a basis-vector e of interest, and returns the probability that the state would be e if a measurement were carried out at that point. It can also be used to query the probability of a set of outcomes, using a map** of just a subset S of the qubits, in which case \(\texttt{prob}\) returns the sum of all probabilities of obtaining a state that satisfies S. For example, if the quantum state computed by a 3-qubit circuit over \(\langle q_0, q_1, q_2 \rangle \) is \(\begin{bmatrix} 0.5&0&0.5&0.5&0&0&0.5&0 \end{bmatrix}\), the user can query the probability of states satisfying \(q_1 = 1 \wedge q_2 = 0\) by calling \(\mathtt{prob({1 : 1, 2 : 0})}\), which would return 0.5 (= \(Pr(q_0 = 0 \wedge q_1 = 1 \wedge q_2 = 0) + Pr(q_0 = 1 \wedge q_1 = 1 \wedge q_2 = 0)\) = \((0.5)^2\) + \((0.5)^2\)).

Given a relational specification R(x, y) and a quantum circuit \(y = Q(x)\), this feature is useful for verifying properties of the form “\(Pr[R(x, Q(x))] > \theta \),” where \(\theta \) is some desired probability threshold for the user’s application.

Debugging Quantum Circuits. Quasimodo additionally provides a feature to query the number of outcomes for a given probability. This feature is especially helpful for debugging large quantum circuits—large in-terms of qubit counts—when most outcomes have similar probabilities.

Consider the case of a quantum circuit whose final quantum state is intended to be \( \frac{1}{\sqrt{6}} \begin{bmatrix} 1&1&1&0&1&1&1&0 \end{bmatrix} \). One can check if the final quantum state is the one intended by querying the number of outcomes that have probability \(\frac{1}{6}\). If the returned value is 6, the user can then check if states 011 and 111 have probability 0 by calling \(\mathtt{prob(\{0: 0, 1: 1, 2:1\})}\) and \(\mathtt{prob(\{0:1, 1:1, 2:1\})}\), respectively. The API function for querying the number of outcomes that have probability \(\texttt {p} \displaystyle \pm \epsilon \) is \(\mathtt{measurement\_counts(p, \epsilon )}\). One can also query the number of outcomes that have probability \(\ge \texttt {p}\) by invoking the function \(\mathtt{tail\_counts(p)}\).

Quasimodo ’s API provides the methods \(\mathtt{get\_state()}\) and \(\mathtt{most\_frequent()}\) to obtain the quantum state (as a pointer to the underlying data-structure) and the outcome with the highest probability, respectively.

3.1 Extending Quasimodo

The currently supported symbolic data-structures for representing quantum states and quantum gates are written in C++ with bindings for Python. All of the current representations implement an abstract C++ class that exposes (i) QuantumState, which returns a state object that represents a quantum state, (ii) eighteen quantum-gate operations, (iii) an operation for gate composition, (iv) an operation for applying a gate—either a primitive gate or the result of gate composition—to a quantum state, and (v) five query operations. Users can easily extend Quasimodo to add a replacement backend by providing an operation to create a state object, as well as implementations of the seventeen gate operations and three query operations. Currently, the easiest path is to implement the custom representation in C++ as an implementation of the abstract C++ class used by Quasimodo ’s standard backends.

4 The Internals of Quasimodo

In this section, we elaborate on the internals of Quasimodo. Specifically, we briefly summarize the BDD, WBDD, and CFLOBDD data-structures that Quasimodo currently supports, and illustrate how Quasimodo performs symbolic simulation using these data-structures. For brevity, we illustrate the way Quasimodo uses these data-structures using the example of the Hadamard gate, a commonly used quantum gate, defined by the matrix \(H = \frac{1}{\sqrt{2}} \begin{bmatrix} 1 &{} 1\\ 1 &{} -1 \end{bmatrix}\).

Fig. 2.
figure 2

Three representations of the Hadamard matrix \(H = \frac{1}{\sqrt{2}} \begin{bmatrix} 1 &{} 1\\ 1 &{} -1 \end{bmatrix}\). (a) A BDD, (b) a CFLOBDD, and (c) a WBDD. The variable ordering is \(\langle x_0, y_0 \rangle \), where \(x_0\) is the row decision variable and \(y_0\) is the column decision variable.

Full size image

Binary Decision Diagrams (BDDs).

Quasimodo provides an option to use Binary Decision Diagrams (BDDs) [3, 5, 7] as the underlying data-structure. A BDD is a data-structure used to efficiently represent a function from Boolean variables to some space of values (Boolean or non-Boolean). The extension of BDDs to support a non-Boolean range is called Multi-Terminal BDDs (MTBDDs) [7] or Algebraic DDs (ADDs) [3]. In this paper, we use “BDD” as a generic term for both BDDs proper and MTBDDs/ADDs. Each node in a BDD corresponds to a specific Boolean variable, and the node’s outgoing edges represents a decision based on the variable’s value (0 or 1). The leaves of the BDD represent the different outputs of the Boolean function. In the best case, BDDs provide an exponential compression in space compared to the size of the decision-tree representation of the function.Footnote 2 Figure 2(a) shows the BDD representation of the Hadamard matrix H with variable ordering \(\langle x_0, y_0 \rangle \), where \(x_0\) is the row decision variable and \(y_0\) is the column decision variable.

We enhanced the CUDD library [12] by incorporating complex numbers at the leaf nodes and adding the ability to count paths.

Context-Free-Language Ordered Binary Decision Diagrams (CFLOBDDs). CFLOBDDs [2]. Whereas a BDD can be considered to be a special form of bounded-size, branching, but non-loo** program, a CFLOBDD can be considered to be a bounded-size, branching, but non-loo** program in which a certain form of procedure call is permitted.

CFLOBDDs can provide an exponential compression over BDDs and double-exponential compression over the decision-tree representation. The additional compression of CFLOBDDs can be roughly attributed to the following reasons:

  • As with BDDs, one level of exponential compression comes from sharing in a directed-acyclic-graph (i.e., a complete binary tree is folded to a dag).

  • In CFLOBDDs, there is a further level of exponential compression from reuse of “procedures”: the same “procedure” can be called multiple times at different call sites.

Such “procedure calls” allow additional sharing of structure beyond what is possible in BDDs: a BDD can share sub-DAGs, whereas a procedure call in a CFLOBDD shares the “middle of a DAG”. The CFLOBDD for Hadamard matrix H, shown in Fig. 2(b), illustrates this concept: the fork node (the node with a split) at the top right of Fig. 2(b) is shared twice—once during the red solid path () and again during the blue dashed path (). The corresponding elements of the BDD for H are outlined in red and blue in Fig. 2(a). The cell entry H[1][1], which corresponds to the assignment \(\{ x_0 \mapsto 1, y_0 \mapsto 1 \}\), is shown in Fig. 2(a) (BDD) and Fig. 2(b) (CFLOBDD) as the paths highlighted in bold that lead to the value \(\frac{-1}{\sqrt{2}}\).

Weighted Binary Decision Diagrams (WBDDs). A Weighted Binary Decision Diagram (WBDD) [9, 14, 19, Ch. 5] is similar to a BDD, but each decision (edge) in the diagram is assigned a weight. To evaluate the represented function f on a given input a (i.e., a is an assignment in \(\{0,1\}^n\)), the path for a is followed; the value of f(a) is the product of the weights encountered along the path. Consider how the WBDD in Fig. 2(c) represents Hadamard matrix H. The variable ordering used is \(\langle x_0, y_0 \rangle \), where \(x_0\) is the row decision variable and \(y_0\) is the column decision variable. Consider the assignment \(a = \{x_0 \mapsto 1, y_0 \mapsto 1\}\). This assignment corresponds to the path shown in red in Fig. 2(c). The WBDD has a weight \(\frac{1}{\sqrt{2}}\) at the root, which is common to all paths. The weight corresponding to \(\{ x_0 \mapsto 1\}\) is 1 and \(\{ y_0 \mapsto 1\}\) is -1; consequently, a evaluates to \(\frac{1}{\sqrt{2}} * 1 * -1 = \frac{-1}{\sqrt{2}}\), which is equal to the value in cell H[1][1].

WBDDs have been used in a variety of applications, such as verification and quantum simulation [19]. In the case of quantum simulation, the weights on the edges of a WBDD are complex numbers. Additionally, the weight on the left-hand edge at every decision node is normalized to 1; this invariant ensures that WBDDs provide a canonical representation of Boolean functions. We use the MQT DD package [19] for backend WBDD support. As distributed, MQT DD supports at most 128 qubits; we modified it to support up to \(2^{31}\) qubits.

Symbolic Simulation. A symbolic simulation of a quantum circuit-computation [11, 13, 19] uses a symbolic representation qs of a quantum state and performs operations on qs that correspond to quantum-circuit operations.

  • A quantum state of n qubits is a vector of size \(2^n \times 1\). Its entries are called amplitudes, and the vector represents the probability distribution given by the squares of the absolute values of the amplitudes. In Quasimodo, CFLOBDDs, BDDs, and WBDDs are used to represent functions of the form \(f: \{ 0,1 \} ^n \rightarrow \mathbb {C}\)—i.e., f is a vector holding complex amplitudes.

  • A quantum gate performs a linear transformation of a quantum state. Quantum-gate application is implemented by using a CFLOBDD, BDD, or WBDD to represent the matrix describing the quantum gate, and performing a matrix-vector multiplication ([11, Sect. 7.6–Sect. 7.7], [3]) of the gate matrix and the quantum state.

  • For CFLOBDDs, BDDs, and WBDDs, operations like prob, measurement_counts, and tail_counts are implemented as exact operations—i.e., no sampling—via projection and path-counting operations ([11, Sect. 7.8], [5]). For CFLOBDDs and BDDs, Quasimodo computes prob via an efficient path-counting operation [11, Sect. 7.8.1 and Sect. 10.1.2, respectively] to obtain the number of paths leading to each terminal value, and then projects the result onto the variables of interest (as specified by the user). Quasimodo then returns the sum of the probabilities of the remaining paths. In the case of WBDDs as the backend, Quasimodo computes the probability of every node ([19, Ch. 5]) instead of counting paths. To compute measurement_counts, Quasimodo returns the number of paths that lead to the requested probability value within the provided threshold \(\epsilon \). On querying tail_counts, Quasimodo returns the number of paths that lead to terminal values having probability \(\texttt {prob} \ge \texttt {p}\), where p is the requested probability.

  • Once path-counts are computed, a measurement from the CFLOBDD, BDD, or WBDD symbolic representation of a quantum state is a data-structure traversal that can be carried out in time proportional to \(\mathcal {O}(\max (\text {number of qubits in the circuit}, \text {size of argument CFLOBDD}))\)

5 Experiments

In this section, we present some experimental results from using Quasimodo on seven quantum benchmarks, Greenberger-Horne-Zeilinger state creation (GHZ), Bernstein-Vazirani algorithm (BV), Deutsch-Jozsa algorithm (DJ), Simon’s algorithm, Grover’s algorithm, Shor’s algorithm (\(2n + 3\) qubits circuit by [4]), and application of the Quantum Fourier Transform (QFT) to a basis state, for different numbers of qubits. Columns 2–4 of Table 1 show the time taken for running the benchmarks with CFLOBDDs, BDDs (CUDD 3.0.0 [12]), and WBDDs (MQT DD v2.1.0 [17]). For each benchmark and number of qubits, we created 50 random oracles and report the average time taken across the 50 runs. For each run of each benchmark, we performed a measurement at the end of the circuit computation and checked if the measured outcome is correct. We ran all of the experiments on AWS machines: t2.xlarge machines with 4 vCPUs, 16GB memory, and a stack size of 8192KB, running on an Ubuntu OS.

One sees that CFLOBDDs scale better than BDDs and WBDDs for the GHZ, BV, and DJ benchmarks as the number of qubits increases. BDDs perform better than CFLOBDDs and are comparable to WBDDs for Simon’s algorithm, whereas WBDDs perform better than BDDs and CFLOBDDs for QFT, Grover’s algorithm, and Shor’s algorithm.

We noticed that the BDD implementation suffers from precision issues; i.e., if an algorithm with a large number of qubits contains too many Hadamard gates, it can lead to extremely low-probability values for each basis state, which are rounded to 0, which in turn causes leaves that really should hold different miniscule values to be coelesced unsoundly, leading to incorrect results. To overcome this issue, one needs to increase the floating-point precision of the floating-point package used to represent BDD leaf values. We increased the precision at 512 qubits (\(^*\)) and again at 2048 qubits (\(^{**}\)).

Table 1. Performance of CFLOBDDs, BDDs, WBDDs using Quasimodo; and other simulators like MQT DDSim, Quimb, and Google Tensor Network (GTN)
Full size table

Part of these results are similar to the work reported in [11]; however, that paper did not use Quasimodo. The results of the present paper were obtained using Quasimodo, and we also report results for WBDDs, as well as BDDs and CFLOBDDs (both of which were used in [11]). The numbers given in Table 1 are slightly different from those given in [11] because these quantum circuits exclusively use gate operations that are applied in sequence to the initial quantum state. One can rewrite the quantum circuit to first compute various gate-gate operations (either Kronecker product or matrix-multiplication operations) and then apply the resultant gate to the initial quantum state. For example, consider a part of a circuit defined as follows:

figure e

Instead of applying CNOT (cx) sequentially for every i, one can construct a gate equivalent to \(cx\_op = \varPi _{i=0}^{n-1}cx(i, n)\) and then apply \(cx\_op\) to quantum state qc as follows:

figure f

Quasimodo supports such operations as Kronecker product and matrix product of two gate matrices. [11] uses such computations for both oracle construction and as part of the quantum algorithm. Table 2 shows the results on GHZ, BV, and DJ algorithms using the same circuit and oracle construction used in [11]. However, Simon’s algorithm, Grover’s algorithm, and Shor’s algorithm in [11] use operations outside Quasimodo ’s computational model, and the results on these benchmarks differ from [11]. (Note that the results reported in Table 2 do not include the time taken for the construction of the oracle.)

Table 2. Performance of CFLOBDDs, BDDs, WBDDs using Quasimodo on an alternate circuit implementation of GHZ, BV, DJ algorithms
Full size table

We also compared Quasimodo with three other quantum-simulation tools: MQT DDSim [18], Quimb [8], and Google Tensor Network (GTN) [10]. MQT DDSim is based on WBDDs (using MQT DD), whereas Quimb and GTN are based on tensor networks. Their performance is shown in columns 6–8 of Table 1. Note that MQT DDSim does not support more than 128 qubits.

6 Conclusion

In this paper, we presented Quasimodo, an extensible, open-source framework for quantum simulation using symbolic data-structures. Quasimodo supports CFLOBDDs and both unweighted and weighted BDDs as the underlying data-structures for representing quantum states and for performing quantum-circuit operations. Quasimodo is implemented as a Python library. It provides an API to commonly used quantum gates and quantum operations, and also supports operations for (i) computing the probability of a measurement leading to a given set of states, (ii) obtaining a representation of the set of states that would be observed with a given probability, and (iii) measuring an outcome from a quantum state.