Optimising Clifford Circuits with Quantomatic

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.

In Proceedings QPL 2018, arXiv:1901.09476

References in corpus (1)

• A universal completion of the ZX-calculus

Cited by in corpus (15)

• A Verified Optimizer for Quantum Circuits
• Review of Distributed Quantum Computing. From single QPU to High Performance Quantum Computing
• A Deductive Verification Framework for Circuit-building Quantum Programs
• Application-Motivated, Holistic Benchmarking of a Full Quantum Computing Stack
• Quantum Circuit Compiler for a Shuttling-Based Trapped-Ion Quantum Computer
• Relating Measurement Patterns to Circuits via Pauli Flow
• Operads for complex system design specification, analysis and synthesis
• Partitioning Quantum Chemistry Simulations with Clifford Circuits
• A Generic Compilation Strategy for the Unitary Coupled Cluster Ansatz
• ZX-Calculus and Extended Wolfram Model Systems II: Fast Diagrammatic Reasoning with an Application to Quantum Circuit Simplification
• Graph Optimization Perspective for Low-Depth Trotter-Suzuki Decomposition
• Completeness of the ZH-calculus
• Completeness of the Phase-free ZH-calculus
• Classical Coding Approaches to Quantum Applications
• Type-Based Verification of Connectivity Constraints in Lattice Surgery