A SAT Encoding for Optimal Clifford Circuit Synthesis

TL;DR

This paper introduces a SAT-based method for the optimal synthesis of Clifford circuits, enabling more efficient quantum circuit compilation by finding minimal gate sequences, which surpasses heuristic methods in performance.

Contribution

The paper presents a novel SAT encoding approach for optimal Clifford circuit synthesis, extending capabilities to larger qubit counts compared to previous methods.

Findings

SAT-based synthesis outperforms heuristics in gate count reduction

Experiments on up to 6 qubits demonstrate effectiveness

State-of-the-art heuristics produce more than twice the gates

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.