Optimising Clifford Circuits with Quantomatic
arXiv:1901.10114 · doi:10.4204/EPTCS.287.5
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 (16)
- Improved Simulation of Stabilizer Circuits
- Instantaneous non-local computation of low T-depth quantum circuits
- The Heisenberg Representation of Quantum Computers
- Interacting Quantum Observables: Categorical Algebra and Diagrammatics
- Determinism in the one-way model
- The ZX-calculus is complete for stabilizer quantum mechanics
- Shorter stabilizer circuits via Bruhat decomposition and quantum circuit transformations
- Pivoting makes the ZX-calculus complete for real stabilizers
- Generators and relations for n-qubit Clifford operators
- A universal completion of the ZX-calculus
- Verifying the Steane code with Quantomatic
- Quantomatic: A Proof Assistant for Diagrammatic Reasoning
- Making the stabilizer ZX-calculus complete for scalars
- Verifying the Smallest Interesting Colour Code with Quantomatic
- A Simplified Stabilizer ZX-calculus
- Supplementarity is Necessary for Quantum Diagram Reasoning
Cited by in corpus (22)
- Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus
- PyZX: Large Scale Automated Diagrammatic Reasoning
- A Verified Optimizer for Quantum Circuits
- Review of Distributed Quantum Computing. From single QPU to High Performance Quantum Computing
- Phase Gadget Synthesis for Shallow Circuits
- The ZX calculus is a language for surface code lattice surgery
- 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
- Logical Clifford Synthesis for Stabilizer Codes
- Operads for complex system design specification, analysis and synthesis
- Relating Measurement Patterns to Circuits via Pauli Flow
- 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
- Verified Optimization in a Quantum Intermediate Representation
- 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
- Circuit Relations for Real Stabilizers: Towards TOF+H