Despite their widespread use in quantum computing and physics, the relative strengths and weaknesses of Matrix Product States (MPS), Decision Diagrams (DDs), and Restricted Boltzmann Machines (RBMs) remains poorly understood. We analytically compare the succinctness of these quantum state representations and analyze the complexity of key operations on them. To overcome shortcomings of the tractability measure, we introduce `rapidity' conditions that identify when non-canonical representations efficiently simulate each other. Our results reveal that: 1. Most DD variants are redundant with respect to MPS in a strong sense; MPS is more rapid. 2. Only one DD variant, called LIMDD, and RBM have succinctness incomparable to MPS. 3. LIMDD and RBM seem to achieve this by sacrificing tractability of counting queries, as shown by a metatheorem on the conditional hardness of these queries.

Abstract We present , a versatile, open-source Python library for quantum circuit analysis. reduces various simulation, verification, and synthesis tasks to weighted model counting (#SAT). It supports universal quantum circuits and a wide variety of gates. provides multiple encodings based on different algebraic bases and equivalence-checking methods, enabling key performance trade-offs. Moreover, the new version of adds approximate equivalence checking, which is crucial in its synthesis algorithms, since it enables translation between arbitrary gate sets. Its synthesis engine is depth-optimal, making it well-suited to real-world quantum computing. This paper demonstrates the design, extensibility, and use of .

Quantum computing has emerged as a transformative force in the evolution of computing technology. Recent efforts have applied quantum techniques to classical database challenges, such as query optimization, data integration, index selection, and transaction management. In this paper, we shift focus to a critical yet underexplored area: data management for quantum computing. We are currently in the noisy intermediate-scale quantum (NISQ) era, where qubits, while promising, are fragile and still limited in scale. After differentiating quantum data from classical data, we outline current and future data management paradigms in the NISQ era and beyond. We address the data management challenges arising from the emerging demands of near-term quantum computing. Our goal is to chart a clear course for future quantum-oriented data management research, establishing it as a cornerstone for the advancement of quantum computing in the NISQ era.

Abstract This tutorial introduces quantum computing with a focus on the applicability of formal methods in this relatively new domain. We describe quantum circuits and convey an understanding of their inherent combinatorial nature and the exponential blow-up that makes them hard to analyze. Then, we show how weighted model counting (#SAT) can be used to solve hard analysis tasks for quantum circuits. This tutorial is aimed at everyone in the formal methods community with an interest in quantum computing. Familiarity with quantum computing is not required, but basic linear algebra knowledge (particularly matrix multiplication and basis vectors) is a prerequisite. The goal of the tutorial is to inspire the community to advance the development of quantum computing with formal methods.

Abstract Verifying equivalence between two quantum circuits is a hard problem, that is nonetheless crucial in compiling and optimizing quantum algorithms for real-world devices. This paper gives a Turing reduction of the (universal) quantum circuits equivalence problem to weighted model counting (WMC). Our starting point is a folklore theorem showing that equivalence checking of quantum circuits can be done in the so-called Pauli-basis. We combine this insight with a WMC encoding of quantum circuit simulation, which we extend with support for the Toffoli gate. Finally, we prove that the weights computed by the model counter indeed realize the reduction. With an open-source implementation, we demonstrate that this novel approach can outperform a state-of-the-art equivalence-checking tool based on ZX calculus and decision diagrams.

Quantum communication enables a host of applications that cannot be achieved by classical communication means, with provably secure communication as one of the prime examples. The distance that quantum communication schemes can cover via direct communication is fundamentally limited by losses on the communication channel. By means of quantum repeaters, the reach of these schemes can be extended and chains of quantum repeaters could in principle cover arbitrarily long distances. In this work, we provide two efficient algorithms for determining the generation time and fidelity of the first generated entangled pair between the end nodes of a quantum repeater chain. The runtime of the algorithms increases polynomially with the number of segments of the chain, which improves upon the exponential runtime of existing algorithms. Our first algorithm is probabilistic and can analyze refined versions of repeater chain protocols which include intermediate entanglement distillation. Our second algorithm computes the waiting time distribution up to a pre-specified truncation time, has faster runtime than the first one and is moreover exact up to machine precision. Using our proof-of-principle implementation, we are able to analyze repeater chains of thousands of segments for some parameter regimes. The algorithms thus serve as useful tools for the analysis of large quantum repeater chain protocols and topologies of the future quantum internet.

Quantum communication brings radically new capabilities that are provably impossible to attain in any classical network. Here, we take the first step from a physics experiment to a quantum internet system. We propose a functional allocation of a quantum network stack, and construct the first physical and link layer protocols that turn ad-hoc physics experiments producing heralded entanglement between quantum processors into a well-defined and robust service. This lays the groundwork for designing and implementing scalable control and application protocols in platform-independent software. To design our protocol, we identify use cases, as well as fundamental and technological design considerations of quantum network hardware, illustrated by considering the state-of-the-art quantum processor platform available to us (Nitrogen-Vacancy (NV) centers in diamond). Using a purpose built discrete-event simulator for quantum networks, we examine the robustness and performance of our protocol using extensive simulations on a supercomputing cluster. We perform a full implementation of our protocol in our simulator, where we successfully validate the physical simulation model against data gathered from the NV hardware. We first observe that our protocol is robust even in a regime of exaggerated losses of classical control messages with only little impact on the performance of the system. We proceed to study the performance of our protocols for 169 distinct simulation scenarios, including trade-offs between traditional performance metrics such as throughput, and the quality of entanglement. Finally, we initiate the study of quantum network scheduling strategies to optimize protocol performance for different use cases.