Exhaustive Search for Quantum Circuit Optimization using ZX Calculus

Quantum computers allow a near-exponential speed-up for specific applications
when compared to classical computers. Despite recent advances in the hardware
of quantum computers, their practical usage is still severely limited due to a
restricted number of available physical qubits and quantum gates, short
coherence time, and high error rates. This paper lays the foundation towards a
metric independent approach to quantum circuit optimization based on exhaustive
search algorithms. This work uses depth-first search and iterative deepening
depth-first search. We rely on ZX calculus to represent and optimize quantum
circuits through the minimization of a given metric (e.g. the T-gate and edge
count). ZX calculus formally guarantees that the semantics of the original
circuit is preserved. As ZX calculus is a non-terminating rewriting system, we
utilise a novel set of pruning rules to ensure termination while still
obtaining high-quality solutions. We provide the first formalization of quantum
circuit optimization using ZX calculus and exhaustive search. We extensively
benchmark our approach on 100 standard quantum circuits. Finally, our
implementation is integrated in the well-known libraries PyZX and Qiskit as a
compiler pass to ensure applicability of our results.