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.
In this work, EQUALITY partners from Leiden University ask the question of how effective the methods motivated by classical automated reasoning can be for quantum compilation. The group assess their current applicability to this new domain by discussing the recent advances. In particular, they focus on three core automated reasoning approaches: decision diagrams, satisfiability and graphical calculus-based methods. In this survey, they 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. The group finds that surprisingly all considered reasoning methods, while originally developed for classical purposes, can excel at various compilation tasks for even universal quantum circuits.
Read the paper: https://doi.org/10.1007/978-3-031-66149-5_6
