ABSTRACT. Tensor networks and circuits are widely used data structures to represent pseudo-Boolean functions. These two formalisms have been studied primarily in separate communities, and this paper aims to establish equivalences between them. We show that some classes of tensor networks that are appealing in practice correspond to classes of circuits with specific properties that have been studied in knowledge compilation as tractable circuits. In particular, we prove that matrix product states (tensor trains) coincide with nondeterministic edge-valued decision diagrams and that tree tensor networks exactly correspond to structured-decomposable circuits. These correspondences enable direct transfer of structural and algorithmic results; for example, canonicity and tractability guarantees known for circuits yield analogous guarantees for the associated tensor networks, and vice versa.

ABSTRACT. We introduce new parallel algorithms for efficient simulation of stabilizer (Clifford) circuits on GPUs. Our approach reformulates key bottlenecks in stabilizer simulation, such as Gaussian elimination and measurement updates, into GPU-tailored primitives that eliminate sequential dependencies and maximize memory coalescing. We implement these techniques in QuaSARQ, a GPU-accelerated stabilizer simulator designed for large qubit counts and many-shot sampling. Across a broad benchmark suite reaching 180,000 qubits and depth 1,000 (roughly 130M gates), QuaSARQ shows substantial runtime improvements, with up to $105\times$ speedup and over 80% energy reduction on demanding instances. Moreover, QuaSARQ consistently outperforms Stim, a state-of-the-art CPU-optimized stabilizer simulator, as well as Qiskit Aer (CPU/GPU), Qibo, Cirq, and PennyLane. These results demonstrate that our parallel algorithms can significantly advance the scalability of stabilizer-circuit simulation, particularly for measurement-heavy and many-shot workloads, while providing a scalable backend for formal analysis, verification, and benchmarking of Clifford circuits.

ABSTRACT. High-dimensional quantum computation needs a native circuit-level equational theory for qudits. We give the first finite schematic equational theory that is sound and complete for exact unitary qudit circuits in every finite dimension at least two. The result is entirely circuit-level: circuits are built from local gates, sequential and parallel composition, and value-controls, and equality is derivable exactly when two circuits have the same standard unitary semantics. For each dimension, the theory is presented by a finite family of local bounded-arity axiom schemata whose diagrammatic shapes are uniform in the dimension. The key syntactic ingredient is primitive value-control, which builds control on a chosen basis value directly into the language. This gives the language a useful internal algebra of controlled operations from local rules while keeping the presentation native to qudit circuits. The result provides a finite, dimension-uniform foundation for exact equational reasoning about qudit circuits.

ABSTRACT. Weighted model counting (WMC) has proven effective across computer science and physics, yet existing applications to quantum physics target only specific problem instances, lacking a general framework with formal guarantees. We present a framework that converts Dirac notation to WMC instances via a type system and denotational semantics, supporting general $q^n \times q^m$ matrix operations including multiplication, addition, and trace. We prove correctness of the encoding and provide a Python implementation. As applications, we compute partition functions of the transverse-field Ising model and the Potts model, demonstrating that heuristics from automated reasoning can be systematically brought to bear on quantum physics.

ABSTRACT. In this work, we introduce a framework for exact classical simulation in noisy quantum circuits based on weighted model counting (WMC), leveraging techniques from automated reasoning to enable efficient classical analysis of quantum computations by exploiting structure within the quantum circuit. Rather than reconstructing the full quantum state, this approach enables the direct computation of targeted quantities of interest, including exact output probabilities and selected density matrix elements even in the presence of general noise processes. To achieve this, we introduce a novel encoding of mixed quantum states within the WMC framework that explicitly represents the density matrix in the computational basis. This representation complements existing Pauli-basis encodings and is shown to be advantageous in specific regimes. Furthermore, we introduce a framework which allows for the translation of arbitrary linear super operators to the weighted model counting framework in both of these encodings. Among other maps, this allows for the formulation of any completely positive trace preserving map in terms of a logical formula. As a result, any physical map, be it unitary (e.g. quantum gates) or non-unitary (e.g. noise channels) can be translated to a weighted model counting problem. This provides a unified approach for simulating quantum dynamics under general discrete operations. We demonstrate the framework on several physically relevant noise channels commonly encountered in quantum hardware, including depolarizing, phase damping, and amplitude damping noise. We evaluate our approach by performing experiments on a benchmark set of randomly generated quantum circuits based on two universal gate sets: the Clifford+T set and the rotational gate set. The performance of the encodings for the universal gate sets and various noise channels are investigated, as well as compared to existing tensor network and decision diagram based simulators. Our results show that our tool generally outperforms these methods and we identify regimes where either encoding outperforms the other, providing guidance on how to select the most effective representation for a given circuit and noise model. Furthermore, the approach also outperforms with respect to weak simulation, i.e. sampling-based methods. This work demonstrates that automated reasoning techniques can serve as a powerful tool for noisy quantum verification, quantum error correction studies, …, providing exact analysis tools for noisy intermediate scale quantum hardware and fault-tolerant quantum computing.

ABSTRACT. Quantum circuit synthesis is an essential part of developing efficient programs for quantum computers. Designing efficient quantum algorithms is a highly complex and non-intuitive process. At the same time, many classes of quantum circuits do not yet have optimal solutions and can potentially be further optimized. The development of quantum computers is an ongoing and important area of research, with various architectures emerging. Each of these architectures, however, supports only a specific set of gates. All of the aforementioned points demonstrate the importance of and demand for efficient, automatic quantum circuit synthesis that enables the creation of circuits with a parametric set of supported gates. Specifically, we consider the creation of new circuits from a specification, as opposed to classical optimization approaches that rewrite an existing circuit. This is a problem with an enormous state space, and many synthesis approaches fail to achieve the required scalability. In this talk, we will present an approach to quantum circuit synthesis that describes the given problem using first-order logic formulae, which are then discharged using SMT or MILP solvers. An important aspect of this work is the use of various representations of complex numbers. Beyond the classical representation using two real numbers, we also support a subset of complex numbers that allow precise algebraic representation using quintuples of integers. This representation allows for more efficient encoding of quantum gates and a formulation using only linear expressions. Among other things, the implemented tool supports various methods of circuit search based on a defined optimization function. Using incremental encoding, we are able to find depth-optimal circuits. We focus on the class of repeat-until-success (RUS) quantum circuits, which can compute unitaries more efficiently than standard techniques using ancillas and measurements. Using the implemented tool, we demonstrate that some RUS circuits from the literature can be further optimized and reduced. The implemented tool is further compared with the state-of-the-art quantum circuit synthesis tool Quokka#. The comparison results show comparable performance between the two approaches.

ABSTRACT. While quantum hardware remains limited, hybrid quantum-classical algorithms with complex control structures, including unbounded loops, are emerging, posing new challenges for program analysis: the accurate estimation of resource consumption of a given program is needed. In this work, we answer this challenge with the first static analysis solution for reasoning about the resources — termination or cost — of hybrid quantum programs with unbounded loops. Towards that end, we introduce integer hybrid path-sums, a symbolic representation of possible executions of a quantum program. A generic strategy for determining termination and expected resource consumption via loop invariants is also proposed. Finally, a prototype of this solution is implemented in Haskell. This work is the first step toward the design of a complete static resource analysis tool for hybrid quantum programs with unbounded loops, essential for the development of real-world quantum computing. This extended abstract illustrates fully developed results without expanding on the technicalities.