# Optimising Clifford Circuits with Quantomatic

arXiv: https://arxiv.org/abs/1901.10114 · HTML: https://mlsanity.com/paper/1901.10114/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 29 Jan 2019.

## Built on by (most cited first, 3 of 3)

- [Quantum Circuit Synthesis and Compilation Optimization: Overview and Prospects](https://mlsanity.com/paper/2407.00736/) (2024)
- [Quantum Circuit Compiler for a Shuttling-Based Trapped-Ion Quantum Computer](https://mlsanity.com/paper/2207.01964/) (2022)
- [Reinforcement Learning for Adaptive Composition of Quantum Circuit Optimisation Passes](https://mlsanity.com/paper/2601.21629/) (2026)

## Abstract (arXiv)

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.