Synthesizing fault-tolerant Clifford circuits using boolean satisfiability

Large-scale quantum computing requires fault-tolerant algorithms to counter hardware noise that would otherwise corrupt information. While the overhead of fault-tolerant quantum computation exceeds current hardware capabilities, optimizing these protocols is crucial for practical implementation. Clifford circuits are fundamental to these protocols, as many universal fault-tolerant quantum computing schemes, such as magic state distillation, utilize the Clifford gate set. Currently, Clifford circuits for fault-tolerant protocols are typically manually designed for specific error correction codes. Inspired by the well-established field of digital circuit design, this work approaches Clifford circuit synthesis using satisfiability-solving techniques. We show the NP-completeness of depth-optimal Clifford synthesis and illustrate how satisfiability solving can synthesize fault-tolerant state-preparation circuits for Calderbank-Shor-Steane codes. This entails both heralded repeat-until-success and deterministic state preparation protocols. The resulting Clifford circuit designs surpass existing constructions and enable state preparation circuits for previously under-explored quantum codes, demonstrating how classical circuit design techniques can advance fault-tolerant quantum computing.