Saved in:
| Main Authors: | , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2604.24504 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917440029458432 |
|---|---|
| author | Huang, Wei-Jia Chareton, Christophe Chen, Yu-Fang Chung, Kai-Min Hsieh, Min-Hsiu Laarman, Alfons Mei, Jingyi |
| author_facet | Huang, Wei-Jia Chareton, Christophe Chen, Yu-Fang Chung, Kai-Min Hsieh, Min-Hsiu Laarman, Alfons Mei, Jingyi |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_24504 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting Huang, Wei-Jia Chareton, Christophe Chen, Yu-Fang Chung, Kai-Min Hsieh, Min-Hsiu Laarman, Alfons Mei, Jingyi Symbolic Computation 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. |
| title | Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting |
| topic | Symbolic Computation |
| url | https://arxiv.org/abs/2604.24504 |