Optimal Clifford Synthesis as Planning

Abstract

With the growing interest in practical quantum computing on noisy quantum hardware, quantum circuit optimization is becoming increasingly important. We consider the optimal synthesis of Clifford circuits, which are important for quantum error correction. While a scalable SAT encoding for Clifford synthesis exists, it only optimizes for the most noisy, i.e., binary quantum gates. That solution tends to add too many unary gates, thus introducing unnecessary noise sources. In this paper, we aim at synthesizing Clifford circuits with minimal binary gate count, and minimal unary gate count as a secondary optimization criterion. Expressing this in a performant SAT encoding is non-trivial. It turns out that planning specifications using PDDL with conditional effects are elegant and allow a flexible specification of costs. However, existing planners struggle on domains with conditional effects. The contribution of this paper is a number of different planning domains to solve the optimal binary/unary Clifford synthesis problem. The best performing solution combines the SAT approach for binary gates with a planning approach for unary gate minimization. As far as we know, this is the first approach that optimizes unary gates without increasing the binary gate count for Clifford circuits. With this hybrid approach, we present improved circuits for famous quantum error correcting codes, such as the Shor code and the Steane code. We believe that our various planning domains with conditional effects and costs form a challenging benchmark for contemporary planners.