Executing quantum algorithms on a quantum computer requires compilation to representations
that conform to all restrictions imposed by the device. Due to device’s limited coherence
times and gate fidelities, the compilation process has to be optimized as much as possible.
To this end, an algorithm’s description first has to be synthesized using the device’s gate
library. In this paper, we consider the optimal synthesis of Clifford circuits—an important
subclass of quantum circuits, with various applications. Such techniques are essential to
establish lower bounds for (heuristic) synthesis methods and gauging their performance.
Due to the huge search space, existing optimal techniques are limited to a maximum of six
qubits. The contribution of this work is twofold: First, we propose an optimal synthesis
method for Clifford circuits based on encoding the task as a satisfiability (SAT) problem
and solving it using a SAT solver in conjunction with a binary search scheme. The resulting
tool is demonstrated …