A SAT Encoding for Optimal Clifford Circuit Synthesis
Abstract
Executing quantum algorithms on a quantum computer requires compilation to representations that conform to all restrictions imposed by the device. Due to devices' 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 practically limited to small qubit counts (around six qubits for typical instances). In this work, 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. Experiments on random instances with up to 6 qubits demonstrate that state-of-the-art heuristics on average produce more than twice the number of gates necessary.
Cite
@article{arxiv.2208.11713,
title = {A SAT Encoding for Optimal Clifford Circuit Synthesis},
author = {Sarah Schneider and Lukas Burgholzer and Robert Wille},
journal= {arXiv preprint arXiv:2208.11713},
year = {2025}
}
Comments
This version corrects doi:10.1145/3566097.3567929. A post-publication review revealed issues in the evaluation that led to non-reproducible scalability claims. We reran a thorough evaluation; the SAT method remains valid but the scalability is corrected from 27 to 6 qubits. Results are reproducible from the scripts at https://github.com/munich-quantum-toolkit/qmap/tree/6a0d8a2/eval/