Equivalence Checking of Quantum Circuits by Model Counting
Fuente:
arXiv
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866916180547076096 |
|---|---|
| author | Mei, Jingyi Coopmans, Tim Bonsangue, Marcello Laarman, Alfons |
| author_facet | Mei, Jingyi Coopmans, Tim Bonsangue, Marcello Laarman, Alfons |
| contents | Verifying equivalence between two quantum circuits is a hard problem, that is nonetheless crucial in compiling and optimizing quantum algorithms for real-world devices. This paper gives a Turing reduction of the (universal) quantum circuits equivalence problem to weighted model counting (WMC). Our starting point is a folklore theorem showing that equivalence checking of quantum circuits can be done in the so-called Pauli-basis. We combine this insight with a WMC encoding of quantum circuit simulation, which we extend with support for the Toffoli gate. Finally, we prove that the weights computed by the model counter indeed realize the reduction. With an open-source implementation, we demonstrate that this novel approach can outperform a state-of-the-art equivalence-checking tool based on ZX calculus and decision diagrams. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_18813 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Equivalence Checking of Quantum Circuits by Model Counting Mei, Jingyi Coopmans, Tim Bonsangue, Marcello Laarman, Alfons Quantum Physics Verifying equivalence between two quantum circuits is a hard problem, that is nonetheless crucial in compiling and optimizing quantum algorithms for real-world devices. This paper gives a Turing reduction of the (universal) quantum circuits equivalence problem to weighted model counting (WMC). Our starting point is a folklore theorem showing that equivalence checking of quantum circuits can be done in the so-called Pauli-basis. We combine this insight with a WMC encoding of quantum circuit simulation, which we extend with support for the Toffoli gate. Finally, we prove that the weights computed by the model counter indeed realize the reduction. With an open-source implementation, we demonstrate that this novel approach can outperform a state-of-the-art equivalence-checking tool based on ZX calculus and decision diagrams. |
| title | Equivalence Checking of Quantum Circuits by Model Counting |
| topic | Quantum Physics |
| url | https://arxiv.org/abs/2403.18813 |