BZPEERReading, trust and collaboration for research
Menu

Discover

GraphFollow connections around a paper, topic or saved view.

Workspaces

HomePick up where your research flow left off.InboxHandle requests, replies and notifications from one place.CollectionsCurate reading lists, evidence sets and shareable dossiers.ResearchSee your private provenance graph, trail and imports.CollaborationMove from discovery into focused discussion rooms.PublishDraft, preview and publish full-text research articles.

Network

ExpertsFind specialists worth following or asking for help.CommunitiesJoin research circles organized around shared work.PartnersSee external organizations active around the same topics.

Opportunities

ListingsBrowse roles, calls and collaborations with clearer fit signals.

Account

Log inReturn to your reading and collaboration workspace.Create accountStart saving work, following people and joining teams.
Log inCreate account

Researcher profile

Lukas Burgholzer

Lukas Burgholzer contributes to research discovery and scholarly infrastructure.

ResearcherAffiliation not importedOpen to collaborate
quant-phEmerging TechnologiesData Structures and AlgorithmsHardware ArchitectureLogic in Computer Science

Trust snapshot

Quick read

Trust 21 - EmergingVerification L1Unclaimed author
14works
0followers
5topics
4close collaborators

Actions

Decide how to stay connected

Follow researcher0

Identity and collaboration

How to connect with this researcher

Claiming links this public author record to a researcher profile and unlocks direct collaboration workflows.

Log in to claim

Direct collaboration

Open a focused conversation when the fit is right

Claim this author entity first to unlock direct invitations.

Research graph

See the researcher in context

Open full explorer

Inspect adjacent work, topics, institutions and collaborators without jumping out to a separate graph page.

Building this graph slice

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

14 published item(s)

preprint2025arXiv

Towards Supporting QIR: Steps for Adopting the Quantum Intermediate Representation

Intermediate representations (IRs) play a crucial role in the software stack of a quantum computer to facilitate efficient optimizations for executing an application on hardware. One of those IRs is the Quantum Intermediate Representation (QIR), which builds on the classical LLVM compiler infrastructure. In this article, we outline different approaches to how QIR can be adopted. This exploration culminates in a demonstration of what it takes to turn an existing quantum circuit simulator into a QIR runtime and that such a transition is less daunting than it might seem at first. We further show that switching to QIR does not entail any performance deficits compared to the original simulator. On the contrary, the presented steps effortlessly allow adding support for arbitrary classical control flow to any classical simulator. We conclude with an outlook on future directions using QIR. The implemented QIR runtime is available under https://github.com/munich-quantum-toolkit/core.

0 citations0 reviewsNo code linkedOpen access
preprint2023arXiv

The Basis of Design Tools for Quantum Computing: Arrays, Decision Diagrams, Tensor Networks, and ZX-Calculus

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Equivalence Checking of Quantum Circuits with the ZX-Calculus

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).

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Limiting the Search Space in Optimal Quantum Circuit Mapping

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Simulation Paths for Quantum Circuit Simulation with Decision Diagrams

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.

0 citations0 reviewsNo code linkedOpen access
preprint2022arXiv

Towards a SAT Encoding for Quantum Circuits: A Journey From Classical Circuits to Clifford Circuits and Beyond

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.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Efficient Construction of Functional Representations for Quantum Algorithms

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.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Handling Non-Unitaries in Quantum Circuit Equivalence Checking

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.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Hybrid Schrödinger-Feynman Simulation of Quantum Circuits With Decision Diagrams

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ödinger-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.

0 citations0 reviewsNo code linkedOpen access
preprint2021arXiv

Tools for Quantum Computing Based on Decision Diagrams

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Characteristics of Reversible Circuits for Error Detection

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Random Stimuli Generation for the Verification of Quantum Circuits

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Verifying Results of the IBM Qiskit Quantum Circuit Compilation Flow

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.

0 citations0 reviewsNo code linkedOpen access
preprint2019arXiv

Mapping Quantum Circuits to IBM QX Architectures Using the Minimal Number of SWAP and H Operations

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.

0 citations0 reviewsNo code linkedOpen access