# Optimising Clifford Circuits with Quantomatic

## TL;DR

This paper introduces a method for optimizing Clifford circuits using the ZX-calculus and the Quantomatic proof assistant, achieving minimal forms for small circuits and demonstrating promising results on larger ones.

## Contribution

It formalizes a set of rewrite rules for Clifford circuits within Quantomatic and proves their effectiveness in circuit minimization, extending optimization capabilities.

## Key findings

- Proves reduction of 1-2 qubit Clifford circuits to minimal form.
- Demonstrates performance on larger Clifford circuits.
- Establishes Quantomatic as a circuit optimization tool.

## Abstract

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.

---
Source: https://tomesphere.com/paper/1901.10114