aqora

Equivalence Checking of Quantum Circuits with the ZX-Calculus

Lukas Burgholzer, Robert Wille

Springer eBooksJan 1, 20260 citations

Fast Equivalence Checking of Quantum Circuits of Clifford Gates

Dimitrios Thanos, Tim J. Coopmans, Alfons Laarman

arXiv:2308.01206Lecture notes in computer scienceJan 1, 202311 citations

Equivalence Checking of Parameterized Quantum Circuits: Verifying the Compilation ofVariational Quantum Algorithms

Lukas Burgholzer, Robert Wille

Springer eBooksJan 1, 20260 citations

Equivalence Checking of Quantum Circuits Based on Dirac Notation in Maude

Canh Minh Do, Kazuhiro Ogata

Lecture notes in computer scienceJan 1, 20243 citations

Quokka#: Quantum Computing with #SAT

Jingyi Mei, Dekel Zak, Muhammad Osama +2 more

We present Quokka#, a versatile, open-source Python library for quantum circuit analysis. Quokka# reduces various simulation, verification, and synthesis tasks to weighted model counting (#SAT). It supports universal quantum circuits and a wide variety of gates. Quokka# provides multiple encodings based on different algebraic bases and equivalence-checking methods, enabling key performance trade-offs. Moreover, the new version of Quokka# adds approximate equivalence checking, which is crucial in its synthesis algorithms, since it enables translation between arbitrary gate sets. Its synthesis engine is depth-optimal, making it well-suited to real-world quantum computing. This paper demonstrates the design, extensibility, and use of Quokka#.We present Quokka#, a versatile, open-source Python library for quantum circuit analysis. Quokka# reduces various simulation, verification, and synthesis tasks to weighted model counting (#SAT). It supports universal quantum circuits and a wide variety of gates. Quokka# provides multiple encodings based on different algebraic bases and equivalence-checking methods, enabling key performance trade-offs. Moreover, the new version of Quokka# adds approximate equivalence checking, which is crucial in its synthesis algorithms, since it enables translation between arbitrary gate sets. Its synthesis engine is depth-optimal, making it well-suited to real-world quantum computing. This paper demonstrates the design, extensibility, and use of Quokka#.

quant-pharXiv:2605.16509May 19, 20260 citations

Equivalence Checking of Quantum Circuits by Model Counting

Jingyi Mei, Tim J. Coopmans, Marcello Bonsangue +1 more

Abstract 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.Abstract 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.

arXiv:2403.18813Lecture notes in computer scienceJan 1, 202415 citations

Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting

Related papers

Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting

Related papers