Equivalence Checking of Quantum Circuits by Model Counting

• DOI: 10.48550/arxiv.2403.18813
• Publication Date: 2024-03-27
• Authors: Jingyi Mei; Tim Coopmans; Marcello Bonsangue; Alfons Laarman
• Keywords: Formal equivalence checking; Logical equivalence

Verifying equivalence between two quantum circuits is a hard problem, that nonetheless crucial in compiling and optimizing algorithms for real-world devices. This paper gives Turing reduction of the (universal) problem to weighted model counting (WMC). Our starting point folklore theorem showing checking can be done so-called Pauli-basis. We combine this insight with WMC encoding circuit simulation, which we extend support Toffoli gate. Finally, prove weights computed by counter indeed realize reduction. With an open-source implementation, demonstrate novel approach outperform state-of-the-art equivalence-checking tool based on ZX calculus decision diagrams.