Optimising Clifford Circuits with Quantomatic
This work addresses circuit optimization in quantum computing, specifically for Clifford circuits, but appears incremental as it builds on existing ZX-calculus and Quantomatic tools.
The authors tackled the problem of optimizing Clifford circuits by developing a system of equations formalized as rewrite rules in the Quantomatic proof assistant, proving it reduces one- or two-qubit circuits to minimal form and showing numerical results for larger circuits.
We present a system of equations between Clifford circuits, all derivable in the ZX-calculus, and formalised as rewrite rules in the Quantomatic proof assistant. By combining these rules with some non-trivial simplification procedures defined in the Quantomatic tactic language, we demonstrate the use of Quantomatic as a circuit optimisation tool. We prove that the system always reduces Clifford circuits of one or two qubits to their minimal form, and give numerical results demonstrating its performance on larger Clifford circuits.