Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting
arXiv:2604.24504 · doi:10.1007/978-3-032-22749-2_21
Abstract
Equivalence checking of quantum circuits is a central verification task in quantum computing, ensuring the correctness of circuit optimizations, hardware mappings, and compilation pipelines. Among the primary symbolic methods for this purpose, the path-sum formalism provides a compact representation with powerful reduction rules that yield a canonical form for the classically simulable Clifford fragment, but confluence fails beyond the Clifford fragment. We introduce a new weighted model counting (WMC) encoding for path-sums and combine it with the existing path-sum reductions to obtain a verifier that is both complete and efficient. Our method applies reductions whenever possible and invokes the WMC-based decision procedure on the residual path-sum, yielding a complete semantic check up to a global phase. We implement the approach and evaluate it on standard benchmarks. Results show that the hybrid method outperforms either component in isolation and competes with state-of-the-art tools.
References in corpus (11)
- Supplementary information for "Quantum supremacy using a programmable superconducting processor"
- Interacting Quantum Observables: Categorical Algebra and Diagrammatics
- MQT Bench: Benchmarking Software and Design Automation Tools for Quantum Computing
- PyZX: Large Scale Automated Diagrammatic Reasoning
- A Deductive Verification Framework for Circuit-building Quantum Programs
- symQV: Automated Symbolic Verification of Quantum Programs
- Equivalence Checking of Parameterized Quantum Circuits: Verifying the Compilation of Variational Quantum Algorithms
- Partial Equivalence Checking of Quantum Circuits
- Linear and non-linear relational analyses for Quantum Program Optimization
- Complete Equational Theories for the Sum-Over-Paths with Unbalanced Amplitudes
- Rewriting and Completeness of Sum-Over-Paths in Dyadic Fragments of Quantum Computing