Search

As quantum computing advances, the complexity of quantum circuits is rapidly increasing, driving the need for robust methods to aid in their design. Equivalence checking plays a vital role in identifying errors that may arise during compilation and optimization of these circuits and is a critical step in quantum circuit verification. In this work, we introduce a novel method based on Matrix Product Operators (MPOs) for determining the equivalence of quantum circuits. Our approach contracts tensorized quantum gates from two circuits into an intermediary MPO, exploiting their reversibility to determine their equivalence or non-equivalence. Our results show that this method offers significant scalability improvements over existing methods, with polynomial scaling in circuit width and depth for the practical use cases we explore. We expect that this work sets the new standard for scalable equivalence checking of quantum circuits and will become a crucial tool for the validation of increasingly complex quantum systems., Comment: 14 pages, 7 figures

Quantum computing holds great promise for surpassing the limits of classical devices in many fields. Despite impressive developments, however, current research is primarily focused on qubits. At the same time, quantum hardware based on multi-level, qudit, systems offers a range of advantages, including expanded gate sets, higher information density, and improved computational efficiency, which might play a key role in overcoming not only the limitations of classical machines but also of current qubit-based quantum devices. However, working with qudits faces challenges not only in experimental control but particularly in algorithm development and quantum software. In this work, we introduce MQT Qudits, an open-source tool, which, as part of the Munich Quantum Toolkit (MQT), is built to assist in designing and implementing applications for mixed-dimensional qudit devices. We specify a standardized language for mixed-dimension systems and discuss circuit specification, compilation to hardware gate sets, efficient circuit simulation, and open challenges. MQT Qudits is available at github.com/cda-tum/mqt-qudits and on pypi at pypi.org/project/mqt.qudits., Comment: 9 pages, 6 figures

Classical representations of quantum states and operations as vectors and matrices are plagued by an exponential growth in memory and runtime requirements for increasing system sizes. Based on their use in classical computing, an alternative data structure known as Decision Diagrams (DDs) has been proposed, which, in many cases, provides both a more compact representation and more efficient computation. In the classical realm, decades of research have been conducted on DDs and numerous variations tailored for specific applications exist. However, DDs for quantum computing are just in their infancy and there is still room for tailoring them to this new technology. In particular, existing representations of DDs require extending all operations in a quantum circuit to the full system size through extension by nodes representing identity matrices. In this work, we make an important step forward for quantum DDs by stripping these identity structures from quantum operations. This significantly reduces the number of nodes required to represent them as well as eases the pressure on key building blocks of their implementation. As a result, we obtain a structure that is more natural for quantum computing and significantly speeds up with computations-with a runtime improvement of up to 70x compared to the state-of-the-art., Comment: 7 pages, 2 figures

Quantum computers are becoming a reality and numerous quantum computing applications with a near-term perspective (e.g., for finance, chemistry, machine learning, and optimization) and with a long-term perspective (e.g., for cryptography or unstructured search) are currently being investigated. However, designing and realizing potential applications for these devices in a scalable fashion requires automated, efficient, and user-friendly software tools that cater to the needs of end users, engineers, and physicists at every level of the entire quantum software stack. Many of the problems to be tackled in that regard are similar to design problems from the classical realm for which sophisticated design automation tools have been developed in the previous decades. The Munich Quantum Toolkit (MQT) is a collection of software tools for quantum computing developed by the Chair for Design Automation at the Technical University of Munich which explicitly utilizes this design automation expertise. Our overarching objective is to provide solutions for design tasks across the entire quantum software stack. This entails high-level support for end users in realizing their applications, efficient methods for the classical simulation, compilation, and verification of quantum circuits, tools for quantum error correction, support for physical design, and more. These methods are supported by corresponding data structures (such as decision diagrams) and core methods (such as SAT encodings/solvers). All of the developed tools are available as open-source implementations and are hosted on https://github.com/cda-tum., Comment: 8 pages, 4 figures, a live version of this document is available at https://mqt.readthedocs.io

Recent experimental achievements have demonstrated the potential of neutral atom architectures for fault-tolerant quantum computing. These architectures feature the dynamic rearrangement of atoms during computation, enabling nearly arbitrary two-dimensional rearrangements. Additionally, they employ a zoned layout with dedicated regions for entangling, storage, and readout. This architecture requires design automation software that efficiently compiles quantum circuits to this hardware and takes care that atoms are in the right place at the right time. In this paper, we initiate this line of work by providing, (1) an abstract model of the novel architecture and, (2) an efficient solution to the routing problem of entangling gates. By this, we aim to maximize the parallelism of entangling gates and minimize the overhead caused by the routing of atoms between zones. In addition to that, we keep the realm of fault-tolerant quantum computing in mind and consider logical qubit arrays, each of which encodes one logical qubit. We implemented the proposed idea as a tool called NALAC and demonstrated its effectiveness and efficiency by showing that it can significantly reduce the routing overhead of logical entangling gates compared to the naive approach. As part of the Munich Quantum Toolkit (MQT), NALAC is publicly available as open-source at https://github.com/cda-tum/mqt-qmap., Comment: 12 pages, 19 figures v2: revised manuscript

Quantum computing has made tremendous improvements in both software and hardware that have sparked interest in academia and industry to realize quantum computing applications. To this end, several steps are necessary: The underlying problem must be encoded in a quantum circuit, a suitable device must be selected to execute it, and it must be compiled accordingly. This compilation step has a significant influence on the quality of the resulting solution. However, current state-of-the-art compilation tools treat the quantum circuit as a sequence of instructions without considering the actual application it realizes -- wasting a yet untapped potential to increase the solution quality. In this work, a different approach is explored that explicitly incorporates the application considered and aims to optimize its solution quality during compilation. Initial results show the benefits of this approach: For an industry-inspired application of a quantum generative model, the proposed approach outperformed Qiskit's most-optimized compilation scheme and led to better solution quality. Therefore, this work presents a first step towards application-aware compilation., Comment: 8 pages, 3 figures, minor changes, to be published at IEEE International Conference on Quantum Software (QSW), 2024

Fueled by recent accomplishments in quantum computing hardware and software, an increasing number of problems from various application domains are being explored as potential use cases for this new technology. Similarly to classical computing, realizing an application on a particular quantum device requires the corresponding (quantum) circuit to be compiled so that it can be executed on the device. With a steadily growing number of available devices and a wide variety of different compilation tools, the number of choices to consider when trying to realize an application is quickly exploding. Due to missing tool support and automation, especially end-users who are not quantum computing experts are easily left unsupported and overwhelmed. In this work, we propose a methodology that allows one to automatically select a suitable quantum device for a particular application and provides an optimized compiler for the selected device. The resulting framework -- called the MQT Predictor -- not only supports end-users in navigating the vast landscape of choices, it also allows mixing and matching compiler passes from various tools to create optimized compilers that transcend the individual tools. Evaluations of an exemplary framework instantiation based on more than 500 quantum circuits and seven devices have shown that -- compared to both Qiskit's and TKET's most optimized compilation flows for all devices -- the MQT Predictor produces circuits within the top-3 out of 14 baselines in more than 98% of cases while frequently outperforming any tested combination by up to 53% when optimizing for expected fidelity. MQT Predictor is publicly available as open-source on GitHub (https://github.com/cda-tum/mqt-predictor) and as an easy-to-use Python package (https://pypi.org/p/mqt.predictor)., Comment: 25 pages, 11 figures, minor adjustments, published in the ACM Transactions on Quantum Computing (TQC)

Efficient methods for the simulation of quantum circuits on classic computers are crucial for their analysis due to the exponential growth of the problem size with the number of qubits. Here we study lumping methods based on bisimulation, an established class of techniques that has been proven successful for (classic) stochastic and deterministic systems such as Markov chains and ordinary differential equations. Forward constrained bisimulation yields a lower-dimensional model which exactly preserves quantum measurements projected on a linear subspace of interest. Backward constrained bisimulation gives a reduction that is valid on a subspace containing the circuit input, from which the circuit result can be fully recovered. We provide an algorithm to compute the constraint bisimulations yielding coarsest reductions in both cases, using a duality result relating the two notions. As applications, we provide theoretical bounds on the size of the reduced state space for well-known quantum algorithms for search, optimization, and factorization. Using a prototype implementation, we report significant reductions on a set of benchmarks. In particular, we show that constrained bisimulation can boost decision-diagram-based quantum circuit simulation by several orders of magnitude, allowing thus for substantial synergy effects., Comment: 20 pages, 1 algorithm, 2 tables

Hundreds of satellites equipped with cameras orbit the Earth to capture images from locations for various purposes. Since the field of view of the cameras is usually very narrow, the optics have to be adjusted and rotated between single shots of different locations. This is even further complicated by the fixed speed -- determined by the satellite's altitude -- such that the decision what locations to select for imaging becomes even more complex. Therefore, classical algorithms for this Satellite Mission Planning Problem (SMPP) have already been proposed decades ago. However, corresponding classical solutions have only seen evolutionary enhancements since then. Quantum computing and its promises, on the other hand, provide the potential for revolutionary improvement. Therefore, in this work, we propose a hybrid classical quantum computing approach to solve the SMPP combining the advantages of quantum hardware with decades of classical optimizer development. Using the Variational Quantum Eigensolver (VQE), Quantum Approximate Optimization Algorithm (QAOA), and its warm-start variant (W-QAOA), we demonstrate the applicability of solving the SMPP for up to 21 locations to choose from. This proof-of-concept -- which is available on GitHub (https://github.com/cda-tum/mqt-problemsolver) as part of the Munich Quantum Toolkit (MQT) -- showcases the potential of quantum computing in this application domain and represents a first step toward competing with classical algorithms in the future., Comment: 6 pages, 6 figures, to be published at International Conference on Quantum Computing and Engineering (QCE), 2023

In order to implement a quantum computing application, problem instances must be encoded into a quantum circuit and then compiled for a specific platform. The lengthy compilation process is a key bottleneck in this workflow, especially for problems that arise repeatedly with a similar yet distinct structure (each of which requires a new compilation run thus far). In this paper, we aim to overcome this bottleneck by proposing a comprehensive pre-compilation technique that tries to minimize the time spent for compiling recurring problems while preserving the solution quality as much as possible. The following concepts underpin the proposed approach: Beginning with a problem class and a corresponding quantum algorithm, a predictive encoding scheme is applied to encode a representative problem instance into a general-purpose quantum circuit for that problem class. Once the real problem instance is known, the previously constructed circuit only needs to be adjusted -- with (nearly) no compilation necessary. Experimental evaluations on QAOA for the MaxCut problem as well as a case study involving a satellite mission planning problem show that the proposed approach significantly reduces the compilation time by several orders of magnitude compared to Qiskit's compilation schemes while maintaining comparable compiled circuit quality. All implementations are available on GitHub (https://github.com/cda-tum/mqt-problemsolver) as part of the Munich Quantum Toolkit (MQT)., Comment: 11 pages, 8 Figures, minor changes, to be published at International Conference on Quantum Computing and Engineering (QCE), 2023

This paper proposes a novel approach to Hamiltonian simulation using Decision Diagrams (DDs), which are an exact representation based on exploiting redundancies in representations of quantum states and operations. While the simulation of Hamiltonians has been studied extensively, scaling these simulations to larger or more complex systems is often challenging and may require approximations or new simulation methods altogether. DDs offer such an alternative that has not yet been applied to Hamiltonian simulation. In this work, we investigate the behavior of DDs for this task. To this end, we review the basics of DDs such as their construction and present how the relevant operations for Hamiltonian simulation are implemented in this data structure -- leading to the first DD-based Hamiltonian simulation approach. Based on several series of evaluations and comparisons, we then discuss insights about the performance of this complementary approach. Overall, these studies show that DDs indeed may offer a promising new data structure which, for certain examples, can provide orders of magnitudes of improvement compared to the state-of-the-art, yet also comes with its own, fundamentally different, limitations., Comment: 12 pages, 4 figures

Circuit synthesis is the task of decomposing a given logical functionality into a sequence of elementary gates. It is (depth-)optimal if it is impossible to achieve the desired functionality with even shorter circuits. Optimal synthesis is a central problem in both quantum and classical hardware design, but also plagued by complexity-theoretic obstacles. Motivated by fault-tolerant quantum computation, we consider the special case of synthesizing blocks of Clifford unitaries. Leveraging entangling input stimuli and the stabilizer formalism allows us to reduce the Clifford synthesis problem to a family of poly-size satisfiability (SAT) problems -- one for each target circuit depth. On a conceptual level, our result showcases that the Clifford synthesis problem is contained in the first level of the polynomial hierarchy ($\mathsf{NP}$), while the classical synthesis problem for logical circuits is known to be complete for the second level of the polynomial hierarchy ($\Sigma_2^{\mathsf{P}}$). Based on this theoretical reduction, we formulate a SAT encoding for depth-optimal Clifford synthesis. We then employ SAT solvers to determine a satisfying assignment or to prove that no such assignment exists. From that, the shortest depth for which synthesis is still possible (optimality) as well as the actual circuit (synthesis) can be obtained. Empirical evaluations show that the optimal synthesis approach yields a substantial depth improvement for random Clifford circuits and Clifford+T circuits for Grover search., Comment: 12 pages, 2 figures, 1 table, implementation publicly available at https://github.com/cda-tum/qmap

In classical computing, error-correcting codes are well established and are ubiquitous both in theory and practical applications. For quantum computing, error-correction is essential as well, but harder to realize, coming along with substantial resource overheads and being concomitant with needs for substantial classical computing. Quantum error-correcting codes play a central role on the avenue towards fault-tolerant quantum computation beyond presumed near-term applications. Among those, color codes constitute a particularly important class of quantum codes that have gained interest in recent years due to favourable properties over other codes. As in classical computing, decoding is the problem of inferring an operation to restore an uncorrupted state from a corrupted one and is central in the development of fault-tolerant quantum devices. In this work, we show how the decoding problem for color codes can be reduced to a slight variation of the well-known LightsOut puzzle. We propose a novel decoder for quantum color codes using a formulation as a MaxSAT problem based on this analogy. Furthermore, we optimize the MaxSAT construction and show numerically that the decoding performance of the proposed decoder achieves state-of-the-art decoding performance on color codes. The implementation of the decoder as well as tools to automatically conduct numerical experiments are publicly available as part of the Munich Quantum Toolkit (MQT) on GitHub., Comment: 17 pages, 10 figures

Classically simulating quantum circuits is crucial when developing or testing quantum algorithms. Due to the underlying exponential complexity, efficient data structures are key for performing such simulations. To this end, tensor networks and decision diagrams have independently been developed with differing perspectives, terminologies, and backgrounds in mind. Although this left designers with two complementary data structures for quantum circuit simulation, thus far it remains unclear which one is the better choice for a given use case. In this work, we (1) consider how these techniques approach classical quantum circuit simulation, and (2) examine their (dis)similarities with regard to their most applicable abstraction level, the desired simulation output, the impact of the computation order, and the ease of distributing the workload. As a result, we provide guidelines for when to better use tensor networks and when to better use decision diagrams in classical quantum circuit simulation., Comment: 7 pages, 4 figures, comments welcome

Quantum computing promises to solve some important problems faster than conventional computations ever could. Currently available NISQ devices on which first practical applications are already executed demonstrate the potential -- with future fault-tolerant quantum hardware for more demanding applications on the horizon. Nonetheless, the advantages in computing power come with challenges to be addressed in the design automation and software development community. In particular, non-quantum representations of states and operations, which provide the basis, e.g., for quantum circuit simulation or verification, require an exponential amount of memory. We propose to use decision diagrams as data structure to conquer the exponential memory requirements in many cases. In this chapter, we review the fundamentals on decision diagrams and highlight their applicability in the tasks of quantum circuit simulation with and without errors as well as in verification of quantum circuits. The tools presented here are all available online as open source projects., Comment: 23 pages, 8 figures. Published in Springer Book "Design Automation of Quantum Computers"

Quantum computing is an emerging technology that has the potential to revolutionize fields such as cryptography, machine learning, optimization, and quantum simulation. However, a major challenge in the realization of quantum algorithms on actual machines is ensuring that the gates in a quantum circuit (i.e., corresponding operations) match the topology of a targeted architecture so that the circuit can be executed while, at the same time, the resulting costs (e.g., in terms of the number of additionally introduced gates, fidelity, etc.) are kept low. This is known as the quantum circuit mapping problem. This summary paper provides an overview of QMAP, an open-source tool that is part of the Munich Quantum Toolkit (MQT) and offers efficient, automated, and accessible methods for tackling this problem. To this end, the paper first briefly reviews the problem. Afterwards, it shows how QMAP can be used to efficiently map quantum circuits to quantum computing architectures from both a user's and a developer's perspective. QMAP is publicly available as open-source at https://github.com/cda-tum/qmap., Comment: 7 pages, 6 figures, invited paper for the International Symposium on Physical Design (ISPD '23)

Quantum computers promise to efficiently solve important problems classical computers never will. However, in order to capitalize on these prospects, a fully automated quantum software stack needs to be developed. This involves a multitude of complex tasks from the classical simulation of quantum circuits, over their compilation to specific devices, to the verification of the circuits to be executed as well as the obtained results. All of these tasks are highly non-trivial and necessitate efficient data structures to tackle the inherent complexity. Starting from rather straight-forward arrays over decision diagrams (inspired by the design automation community) to tensor networks and the ZX-calculus, various complementary approaches have been proposed. This work provides a look "under the hood" of today's tools and showcases how these means are utilized in them, e.g., for simulation, compilation, and verification of quantum circuits., Comment: 6 pages, 3 figures, Invited paper at the Design Automation Conference 2022

Solving real-world optimization problems with quantum computing requires choosing between a large number of options concerning formulation, encoding, algorithm and hardware. Finding good solution paths is challenging for end users and researchers alike. We propose a framework designed to identify and recommend the best-suited solution paths. This introduces a novel abstraction layer that is required to make quantum-computing-assisted solution techniques accessible to end users without requiring a deeper knowledge of quantum technologies. State-of-the-art hybrid algorithms, encoding and decomposition techniques can be integrated in a modular manner and evaluated using problem-specific performance metrics. Equally, tools for the graphical analysis of variational quantum algorithms are developed. Classical, fault tolerant quantum and quantum-inspired methods can be included as well to ensure a fair comparison resulting in useful solution paths. We demonstrate and validate our approach on a selected set of options and illustrate its application on the capacitated vehicle routing problem (CVRP). We also identify crucial requirements and the major design challenges for the proposed automation layer within a quantum-assisted solution workflow for optimization problems., Comment: Reviewed and published at IEEE QSW 2023

Reversible circuits form the backbone for many promising emerging technologies such as quantum computing, low power/adiabatic design, encoder/decoder devices, and several other applications. In the recent years, the scalable synthesis of such circuits has gained significant attention. In this work, we present the SyReC Synthesizer, a synthesis tool for reversible circuits based on the hardware description language SyReC. SyReC allows to describe reversible functionality at a high level of abstraction. The provided SyReC Synthesizer then realizes this functionality in a push-button fashion. Corresponding options allow for a trade-off between the number of needed circuit signals/lines (relevant, e.g., for quantum computing in which every circuit line corresponds to a qubit) and the respectively needed gates (corresponding to the circuit's costs). Furthermore, the tool allows to simulate the resulting circuit as well as to determine the gate costs of it. The SyReC Synthesizer is available as an open-source software package at https://github.com/cda-tum/syrec as part of the Munich Quantum Toolkit (MQT)., Comment: 6 pages, 3 figures, Software Impacts Journal

Any quantum computing application, once encoded as a quantum circuit, must be compiled before being executable on a quantum computer. Similar to classical compilation, quantum compilation is a sequential process with many compilation steps and numerous possible optimization passes. Despite the similarities, the development of compilers for quantum computing is still in its infancy -- lacking mutual consolidation on the best sequence of passes, compatibility, adaptability, and flexibility. In this work, we take advantage of decades of classical compiler optimization and propose a reinforcement learning framework for developing optimized quantum circuit compilation flows. Through distinct constraints and a unifying interface, the framework supports the combination of techniques from different compilers and optimization tools in a single compilation flow. Experimental evaluations show that the proposed framework -- set up with a selection of compilation passes from IBM's Qiskit and Quantinuum's TKET -- significantly outperforms both individual compilers in 73% of cases regarding the expected fidelity. The framework is available on GitHub (https://github.com/cda-tum/MQTPredictor) as part of the Munich Quantum Toolkit (MQT)., Comment: 6 pages, 3 figures, minor changes, to be published at Design Automation Conference (DAC), 2023

Quantum computing is fast evolving as a technology due to recent advances in hardware, software, as well as the development of promising applications. To use this technology for solving specific problems, a suitable quantum algorithm has to be determined, the problem has to be encoded in a form suitable for the chosen algorithm, it has to be executed, and the result has to be decoded. To date, each of these tedious and error-prone steps is conducted in a mostly manual fashion. This creates a high entry barrier for using quantum computing -- especially for users with little to no expertise in that domain. In this work, we envision a framework that aims to lower this entry barrier by allowing users to employ quantum computing solutions in an automatic fashion. To this end, interfaces as similar as possible to classical solvers are provided, while the quantum steps of the workflow are shielded from the user as much as possible by a fully automated backend. To demonstrate the feasibility and usability of such a framework, we provide proof-of-concept implementations for two different classes of problems which are publicly available on GitHub (https://github.com/cda-tum/MQTProblemSolver) as part of the Munich Quantum Toolkit (MQT). By this, this work provides the foundation for a low-threshold approach realizing quantum computing solutions with no or only moderate expertise in this technology., Comment: 7 pages, 4 figures, minor changes, to be published at International Symposium on Multiple-Valued Logic (ISMVL), 2023

Variational quantum algorithms have been introduced as a promising class of quantum-classical hybrid algorithms that can already be used with the noisy quantum computing hardware available today by employing parameterized quantum circuits. Considering the non-trivial nature of quantum circuit compilation and the subtleties of quantum computing, it is essential to verify that these parameterized circuits have been compiled correctly. Established equivalence checking procedures that handle parameter-free circuits already exist. However, no methodology capable of handling circuits with parameters has been proposed yet. This work fills this gap by showing that verifying the equivalence of parameterized circuits can be achieved in a purely symbolic fashion using an equivalence checking approach based on the ZX-calculus. At the same time, proofs of inequality can be efficiently obtained with conventional methods by taking advantage of the degrees of freedom inherent to parameterized circuits. We implemented the corresponding methods and proved that the resulting methodology is complete. Experimental evaluations (using the entire parametric ansatz circuit library provided by Qiskit as benchmarks) demonstrate the efficacy of the proposed approach. The implementation is open source and publicly available as part of the equivalence checking tool QCEC (https://github.com/cda-tum/qcec) which is part of the Munich Quantum Toolkit (MQT)., Comment: 7 pages, 3 figures, 2 tables, 28th Asia and South Pacific Design Automation Conference (ASPDAC '23)

Compiling a high-level quantum circuit down to a low-level description that can be executed on state-of-the-art quantum computers is a crucial part of the software stack for quantum computing. One step in compiling a quantum circuit to some device is quantum circuit mapping, where the circuit is transformed such that it complies with the architecture's limited qubit connectivity. Because the search space in quantum circuit mapping grows exponentially in the number of qubits, it is desirable to consider as few of the device's physical qubits as possible in the process. Previous work conjectured that it suffices to consider only subarchitectures of a quantum computer composed of as many qubits as used in the circuit. In this work, we refute this conjecture and establish criteria for judging whether considering larger parts of the architecture might yield better solutions to the mapping problem. We show that determining subarchitectures that are of minimal size, i.e., of which no physical qubit can be removed without losing the optimal mapping solution for some quantum circuit, is a very hard problem. Based on a relaxation of the criteria for optimality, we introduce a relaxed consideration that still maintains optimality for practically relevant quantum circuits. Eventually, this results in two methods for computing near-optimal sets of subarchitectures$\unicode{x2014}$providing the basis for efficient quantum circuit mapping solutions. We demonstrate the benefits of this novel method for state-of-the-art quantum computers by IBM, Google and Rigetti., Comment: 19 pages, 9 figures, 3 tables

Any potential application of quantum computing, once encoded as a quantum circuit, needs to be compiled in order to be executed on a quantum computer. Deciding which qubit technology, which device, which compiler, and which corresponding settings are best for the considered problem -- according to a measure of goodness -- requires expert knowledge and is overwhelming for end-users from different domains trying to use quantum computing to their advantage. In this work, we treat the problem as a statistical classification task and explore the utilization of supervised machine learning techniques to optimize the compilation of quantum circuits. Based on that, we propose a framework that, given a quantum circuit, predicts the best combination of these options and, therefore, automatically makes these decisions for end-users. Experimental evaluations show that, considering a prototypical setting with 3000 quantum circuits, the proposed framework yields promising results: for more than three quarters of all unseen test circuits, the best combination of compilation options is determined. Moreover, for more than 95% of the circuits, a combination of compilation options within the top-three is determined -- while the median compilation time is reduced by more than one order of magnitude. Furthermore, the resulting methodology not only provides end-users with a prediction of the best compilation options, but also provides means to extract explicit knowledge from the machine learning technique. This knowledge helps in two ways: it lays the foundation for further applications of machine learning in this domain and, also, allows one to quickly verify whether a machine learning algorithm is reasonably trained. The corresponding framework and the pre-trained classifier are publicly available on GitHub (https://github.com/cda-tum/MQTPredictor) as part of the Munich Quantum Toolkit (MQT)., Comment: 11 pages, 6 figures, minor changes, to be published at IEEE International Conference on Quantum Software (QSW), 2023

Quantum Error Correction (QEC) is an essential field of research towards the realization of large-scale quantum computers. On the theoretical side, a lot of effort is put into designing error-correcting codes that protect quantum data from errors, which inevitably happen due to the noisy nature of quantum hardware and quantum bits (qubits). Protecting data with an error-correcting code necessitates means to recover the original data, given a potentially corrupted data set-a task referred to as decoding. It is vital that decoding algorithms can recover error-free states in an efficient manner. While theoretical properties of recent QEC methods have been extensively studied, good techniques to analyze their performance in practically more relevant settings is still a widely unexplored area. In this work, we propose a set of software tools that allows to numerically experiment with so-called Quantum Low-Density Parity Check codes (QLDPC codes)-a broad class of codes, some of which have recently been shown to be asymptotically good. Based on that, we provide an implementation of a general decoder for QLDPC codes. On top of that, we propose an efficient heuristic decoder that tackles the runtime bottlenecks of the general QLDPC decoder while still maintaining comparable decoding performance. These tools eventually allow to confirm theoretical results around QLDPC codes in a more practical setting and showcase the value of software tools (in addition to theoretical considerations) for investigating codes for practical applications. The resulting tool, which is publicly available at https://github.com/lucasberent/qecc under the MIT license, is meant to provide a playground for the search for "practically good" quantum codes., Comment: 6 pages, 5 figures

As state-of-the-art quantum computers are capable of running increasingly complex algorithms, the need for automated methods to design and test potential applications rises. Equivalence checking of quantum circuits is an important, yet hardly automated, task in the development of the quantum software stack. Recently, new methods have been proposed that tackle this problem from widely different perspectives. One of them is based on the ZX-calculus, a graphical rewriting system for quantum computing. However, the power and capability of this equivalence checking method has barely been explored. The aim of this work is to evaluate the ZX-calculus as a tool for equivalence checking of quantum circuits. To this end, it is demonstrated how the ZX-calculus based approach for equivalence checking can be expanded in order to verify the results of compilation flows and optimizations on quantum circuits. It is also shown that the ZX-calculus based method is not complete$\unicode{x2014}$especially for quantum circuits with ancillary qubits. In order to properly evaluate the proposed method, we conduct a detailed case study by comparing it to two other state-of-the-art methods for equivalence checking: one based on path-sums and another based on decision diagrams. The proposed methods have been integrated into the publicly available QCEC tool (https://github.com/cda-tum/qcec) which is part of the Munich Quantum Toolkit (MQT)., Comment: 15 pages, 12 figures, to be published in IEEE Journal on Emerging and Selected Topics in Circuits and Systems

Executing quantum algorithms on a quantum computer requires compilation to representations that conform to all restrictions imposed by the device. Due to device's limited coherence times and gate fidelities, the compilation process has to be optimized as much as possible. To this end, an algorithm's description first has to be synthesized using the device's gate library. In this paper, we consider the optimal synthesis of Clifford circuits -- an important subclass of quantum circuits, with various applications. Such techniques are essential to establish lower bounds for (heuristic) synthesis methods and gauging their performance. Due to the huge search space, existing optimal techniques are limited to a maximum of six qubits. The contribution of this work is twofold: First, we propose an optimal synthesis method for Clifford circuits based on encoding the task as a satisfiability (SAT) problem and solving it using a SAT solver in conjunction with a binary search scheme. The resulting tool is demonstrated to synthesize optimal circuits for up to $26$ qubits -- more than four times as many as the current state of the art. Second, we experimentally show that the overhead introduced by state-of-the-art heuristics exceeds the lower bound by $27\%$ on average. The resulting tool is publicly available at https://github.com/cda-tum/qmap., Comment: 7 pages, 4 figures

Quantum software tools for a wide variety of design tasks on and across different levels of abstraction are crucial in order to eventually realize useful quantum applications. This requires practical and relevant benchmarks for new software tools to be empirically evaluated and compared to the current state of the art. Although benchmarks for specific design tasks are commonly available, the demand for an overarching cross-level benchmark suite has not yet been fully met and there is no mutual consolidation in how quantum software tools are evaluated thus far. In this work, we propose the MQT Bench benchmark suite (as part of the Munich Quantum Toolkit, MQT) based on four core traits: (1) cross-level support for different abstraction levels, (2) accessibility via an easy-to-use web interface (https://www.cda.cit.tum.de/mqtbench) and a Python package, (3) provision of a broad selection of benchmarks to facilitate generalizability, as well as (4) extendability to future algorithms, gate-sets, and hardware architectures. By comprising more than 70,000 benchmark circuits ranging from 2 to 130 qubits on four abstraction levels, MQT Bench presents a first step towards benchmarking different abstraction levels with a single benchmark suite to increase comparability, reproducibility, and transparency., Comment: 14 pages, 4 figures, MQT Bench is hosted at https://www.cda.cit.tum.de/mqtbench/, revised layout and updated tool

Simulating quantum circuits on classical computers is a notoriously hard, yet increasingly important task for the development and testing of quantum algorithms. In order to alleviate this inherent complexity, efficient data structures and methods such as tensor networks and decision diagrams have been proposed. However, their efficiency heavily depends on the order in which the individual computations are performed. For tensor networks the order is defined by so-called contraction plans and a plethora of methods has been developed to determine suitable plans. On the other hand, simulation based on decision diagrams is mostly conducted in a straight-forward, i.e., sequential, fashion thus far. In this work, we study the importance of the path that is chosen when simulating quantum circuits using decision diagrams and show, conceptually and experimentally, that choosing the right simulation path can make a vast difference in the efficiency of classical simulations using decision diagrams. We propose an open-source framework (available at github.com/cda-tum/ddsim) that not only allows to investigate dedicated simulation paths, but also to re-use existing findings, e.g., obtained from determining contraction plans for tensor networks. Experimental evaluations show that translating strategies from the domain of tensor networks may yield speedups of several factors compared to the state of the art. Furthermore, we design a dedicated simulation path heuristic that allows to improve the performance even further -- frequently yielding speedups of several orders of magnitude. Finally, we provide an extensive discussion on what can be learned from tensor networks and what cannot., Comment: 10 Pages, 7 Figures, 1 Table, Journal Extension to "Exploiting Arbitrary Paths for the Simulation of Quantum Circuits with Decision Diagrams" Design, Automation and Test in Europe Conference (DATE), 2022. Published in the IEEE Transactions on Computer Aided Design of Integrated Circuits and Systems (TCAD)

Satisfiability Testing (SAT) techniques are well-established in classical computing where they are used to solve a broad variety of problems, e.g., in the design of classical circuits and systems. Analogous to the classical realm, quantum algorithms are usually modelled as circuits and similar design tasks need to be tackled. Thus, it is natural to pose the question whether these design tasks in the quantum realm can also be approached using SAT techniques. To the best of our knowledge, no SAT formulation for arbitrary quantum circuits exists and it is unknown whether such an approach is feasible at all. In this work, we define a propositional SAT encoding that, in principle, can be applied to arbitrary quantum circuits. However, we show that due to the inherent complexity of representing quantum states, constructing such an encoding is not feasible in general. Therefore, we establish general criteria for determining the feasibility of the proposed encoding and identify classes of quantum circuits fulfilling these criteria. We explicitly demonstrate how the proposed encoding can be applied to the class of Clifford circuits as a representative. Finally, we empirically demonstrate the applicability and efficiency of the proposed encoding for Clifford circuits. With these results, we lay the foundation for continuing the ongoing success of SAT in classical circuit and systems design for quantum circuits., Comment: 17 pages, 6 figures

Executing quantum circuits on currently available quantum computers requires compiling them to a representation that conforms to all restrictions imposed by the targeted architecture. Due to the limited connectivity of the devices' physical qubits, an important step in the compilation process is to map the circuit in such a way that all its gates are executable on the hardware. Existing solutions delivering optimal solutions to this task are severely challenged by the exponential complexity of the problem. In this paper, we show that the search space of the mapping problem can be limited drastically while still preserving optimality. The proposed strategies are generic, architecture-independent, and can be adapted to various mapping methodologies. The findings are backed by both, theoretical considerations and experimental evaluations. Results confirm that, by limiting the search space, optimal solutions can be determined for instances that timeouted before or speed-ups of up to three orders of magnitude can be achieved., Comment: 7 pages, 5 figures, Asia and South Pacific Design Automation Conference (ASP-DAC), 2022; v2: fixed citation

With quantum computers promising advantages even in the near-term NISQ era, there is a lively community that develops software and toolkits for the design of corresponding quantum circuits. Although the underlying problems are different, expertise from the design automation community, which developed sophisticated design solutions for the conventional realm in the past decades, can help here. In this respect, decision diagrams provide a promising foundation for tackling many design tasks such as simulation, synthesis, and verification of quantum circuits. However, users of the corresponding tools often do not have a proper background or an intuition about how these methods based on decision diagrams work and what their strengths and limits are. In this work, we first review the concepts of how decision diagrams can be employed, e.g., for the simulation and verification of quantum circuits. Afterwards, in an effort to make decision diagrams for quantum computing more accessible, we then present a visualization tool for quantum decision diagrams, which allows users to explore the behavior of decision diagrams in the design tasks mentioned above. Finally, we present decision diagram-based tools for simulation and verification of quantum circuits using the methods discussed above as part of the open-source JKQ quantum toolset---a set of tools for quantum computing developed at the Johannes Kepler University (JKU) Linz and released under the MIT license. More information about the corresponding tools is available at https://github.com/iic-jku/. By this, we provide an introduction of the concepts and tools for potential users who would like to work with them as well as potential developers aiming to extend them., Comment: 16 pages, 10 figures, to be published in the ACM Transactions on Quantum Computing special issue on software tools for quantum computing

Quantum computers are reaching a level where interactions between classical and quantum computations can happen in real-time. This marks the advent of a new, broader class of quantum circuits: dynamic quantum circuits. They offer a broader range of available computing primitives that lead to new challenges for design tasks such as simulation, compilation, and verification. Due to the non-unitary nature of dynamic circuit primitives, most existing techniques and tools for these tasks are no longer applicable in an out-of-the-box fashion. In this work, we discuss the resulting consequences for quantum circuit verification, specifically equivalence checking, and propose two different schemes that eventually allow to treat the involved circuits as if they did not contain non-unitaries at all. As a result, we demonstrate methodically, as well as, experimentally that existing techniques for verifying the equivalence of quantum circuits can be kept applicable for this broader class of circuits., Comment: 7 pages, 4 figures, old title: "Towards Verification of Dynamic Quantum Circuits", revised manuscript, added experimental results

Classical simulations of quantum computations are vital for the future development of this emerging technology. To this end, decision diagrams have been proposed as a complementary technique which frequently allows to tackle the inherent exponential complexity of these simulations. In the worst case, however, they still cannot escape this complexity. Additionally, while other techniques make use of all the available processing power, decision diagram-based simulation to date cannot exploit the many processing units of today's systems. In this work, we show that both problems can be tackled together by employing a hybrid Schr\"odinger-Feynman scheme for the simulation. More precisely, we show that realizing such a scheme with decision diagrams is indeed possible, we discuss the resulting problems in its realization, and propose solutions how they can be handled. Experimental evaluations confirm that this significantly advances the state of the art in decision diagram-based simulation -- allowing to simulate certain hard circuits within minutes that could not be simulated in a whole day thus far., Comment: 8 pages, 5 figures

Due to the significant progress made in the implementation of quantum hardware, efficient methods and tools to design corresponding algorithms become increasingly important. Many of these tools rely on functional representations of certain building blocks or even entire quantum algorithms which, however, inherently exhibit an exponential complexity. Although several alternative representations have been proposed to cope with this complexity, the construction of those representations remains a bottleneck. In this work, we propose solutions for efficiently constructing representations of quantum functionality based on the idea of conducting as many operations as possible on as small as possible intermediate representations -- using Decision Diagrams as a representative functional description. Experimental evaluations show that applying these solutions allows to construct the desired representations several factors faster than with state-of-the-art methods. Moreover, if repeating structures (which frequently occur in quantum algorithms) are explicitly exploited, exponential improvements are possible -- allowing to construct the functionality of certain algorithms within seconds, whereas the state of the art fails to construct it in an entire day., Comment: 15 pages, 5 figures

In this work, we consider error detection via simulation for reversible circuit architectures. We rigorously prove that reversibility augments the performance of this simple error detection protocol to a considerable degree. A single randomly generated input is guaranteed to unveil a single error with a probability that only depends on the size of the error, not the size of the circuit itself. Empirical studies confirm that this behavior typically extends to multiple errors as well. In conclusion, reversible circuits offer characteristics that reduce masking effects -- a desirable feature that is in stark contrast to irreversible circuit architectures., Comment: 6 pages, 9 figures

Verification of quantum circuits is essential for guaranteeing correctness of quantum algorithms and/or quantum descriptions across various levels of abstraction. In this work, we show that there are promising ways to check the correctness of quantum circuits using simulative verification and random stimuli. To this end, we investigate how to properly generate stimuli for efficiently checking the correctness of a quantum circuit. More precisely, we introduce, illustrate, and analyze three schemes for quantum stimuli generation---offering a trade-off between the error detection rate (as well as the required number of stimuli) and efficiency. In contrast to the verification in the classical realm, we show (both, theoretically and empirically) that even if only a few randomly-chosen stimuli (generated from the proposed schemes) are considered, high error detection rates can be achieved for quantum circuits. The results of these conceptual and theoretical considerations have also been empirically confirmed---with a grand total of approximately $10^6$ simulations conducted across 50 000 benchmark instances., Comment: 6 pages, in Asia and South Pacific Design Automation Conference (ASP-DAC) 2021

Realizing a conceptual quantum algorithm on an actual physical device necessitates the algorithm's quantum circuit description to undergo certain transformations in order to adhere to all constraints imposed by the hardware. In this regard, the individual high-level circuit components are first synthesized to the supported low-level gate-set of the quantum computer, before being mapped to the target's architecture---utilizing several optimizations in order to improve the compilation result. Specialized tools for this complex task exist, e.g., IBM's Qiskit, Google's Cirq, Microsoft's QDK, or Rigetti's Forest. However, to date, the circuits resulting from these tools are hardly verified, which is mainly due to the immense complexity of checking if two quantum circuits indeed realize the same functionality. In this paper, we propose an efficient scheme for quantum circuit equivalence checking---specialized for verifying results of the IBM Qiskit quantum circuit compilation flow. To this end, we combine characteristics unique to quantum computing, e.g., its inherent reversibility, and certain knowledge about the compilation flow into a dedicated equivalence checking strategy. Experimental evaluations confirm that the proposed scheme allows to verify even large circuit instances with tens of thousands of operations within seconds or even less, whereas state-of-the-art techniques frequently time-out or require substantially more runtime. A corresponding open source implementation of the proposed method is publicly available at https://github.com/iic-jku/qcec., Comment: 10 pages, to be published at International Conference on Quantum Computing and Engineering (QCE20)

Quantum computing will change the way we tackle certain problems. It promises to dramatically speed-up many chemical, financial, and machine-learning applications. However, to capitalize on those promises, complex design flows composed of steps such as compilation, decomposition, or mapping need to be employed before being able to execute a conceptual quantum algorithm on an actual device. This results in descriptions at various levels of abstraction which may significantly differ from each other. The complexity of the underlying design problems necessitates to not only provide efficient solutions for the single steps, but also to verify that the originally intended functionality is preserved throughout all levels of abstraction. This motivates methods for equivalence checking of quantum circuits. However, most existing methods are inspired by the classical realm and have merely been extended to support quantum circuits (i.e., circuits which do not only rely on 0's and 1's, but also employ superposition and entanglement). In this work, we propose an advanced methodology which takes the different paradigms of quantum circuits not only as a burden, but as an opportunity. In fact, the proposed methodology explicitly utilizes characteristics unique to quantum computing in order to overcome the shortcomings of existing approaches. We show that, by exploiting the reversibility of quantum circuits, complexity can be kept feasible in many cases. Moreover, we show that, in contrast to the classical realm, simulation is very powerful in verifying quantum circuits. Experimental evaluations confirm that the resulting methodology allows one to conduct equivalence checking dramatically faster than ever before--in many cases just a single simulation run is sufficient. An implementation of the proposed methodology is publicly available at https://iic.jku.at/eda/research/quantum_verification/., Comment: 14 pages, 10 figures

The recent progress in the physical realization of quantum computers (the first publicly available ones--IBM's QX architectures--have been launched in 2017) has motivated research on automatic methods that aid users in running quantum circuits on them. Here, certain physical constraints given by the architectures which restrict the allowed interactions of the involved qubits have to be satisfied. Thus far, this has been addressed by inserting SWAP and H operations. However, it remains unknown whether existing methods add a minimum number of SWAP and H operations or, if not, how far they are away from that minimum--an NP-complete problem. In this work, we address this by formulating the mapping task as a symbolic optimization problem that is solved using reasoning engines like Boolean satisfiability solvers. By this, we do not only provide a method that maps quantum circuits to IBM's QX architectures with a minimal number of SWAP and H operations, but also show by experimental evaluation that the number of operations added by IBM's heuristic solution exceeds the lower bound by more than 100% on average. An implementation of the proposed methodology is publicly available at http://iic.jku.at/eda/research/ibm_qx_mapping.