Thanos, D. et al. (2025). Automated Reasoning in Quantum Circuit Compilation. In Model Checking Software. SPIN 2024. Lecture Notes in Computer Science, vol 14624. doi: 10.1007/978-3-031-66149-5_6
Abstract: Automated reasoning techniques have been proven of immense importance in classical applications like formal verification, circuit design and probabilistic inference. The domain of quantum computing poses new challenges of a different nature, such as the compilation of quantum circuits, which involves “quantum-hard” tasks such as the simulation, optimization, synthesis, and equivalence checking of quantum circuits. We ask the question of how effective the methods motivated by classical automated reasoning can be for quantum compilation. We assess their current applicability to this new domain by discussing the recent advances. In particular, we focus on three core automated reasoning approaches: decision diagrams, satisfiability and graphical calculus-based methods. In this survey, we explain in a manner accessible to those unfamiliar with quantum computing concepts how these prominent automated reasoning methods have found numerous applications in quantum circuit compilation. We find that surprisingly all considered reasoning methods, while originally developed for classical purposes, can excel at various compilation tasks for even universal quantum circuits.
