FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams

Abstract

Applications of decision diagrams in quantum circuit analysis have been an active research area. Our work introduces FeynmanDD, a new method utilizing standard and multi-terminal decision diagrams for quantum circuit simulation and equivalence checking. Unlike previous approaches that exploit patterns in quantum states and operators, our method explores useful structures in the path integral formulation, essentially transforming the analysis into a counting problem. The method then employs efficient counting algorithms using decision diagrams as its underlying computational engine. Through comprehensive theoretical analysis and numerical experiments, we demonstrate FeynmanDD's capabilities and limitations in quantum circuit analysis, highlighting the value of this new BDD-based approach.

26 pages, 2 figures, 7 tables. Published in the Proceedings of CAV 2025. Code available at https://github.com/cqs-thu/feynman-decision-diagram

References in corpus (14)

• Supplementary information for "Quantum supremacy using a programmable superconducting processor"
• Improved Simulation of Stabilizer Circuits
• Simulating quantum computation by contracting tensor networks
• Automated optimization of large quantum circuits with continuous parameters
• Exact synthesis of multiqubit Clifford+T circuits
• Towards Large-scale Functional Verification of Universal Quantum Circuits
• A Deductive Verification Framework for Circuit-building Quantum Programs
• Equivalence Checking of Quantum Circuits with the ZX-Calculus
• Quantum circuits and low-degree polynomials over F_2
• A Case for Synthesis of Recursive Quantum Unitary Programs
• Complete Equational Theories for the Sum-Over-Paths with Unbalanced Amplitudes
• Efficient Binary Decision Diagram Manipulation in External Memory
• Rewriting and Completeness of Sum-Over-Paths in Dyadic Fragments of Quantum Computing
• Simulating Quantum Circuits by Model Counting