  Circuit synthesis is the task of decomposing a given logical functionality
into a sequence of elementary gates. It is (depth-)optimal if it is impossible
to achieve the desired functionality with even shorter circuits. Optimal
synthesis is a central problem in both quantum and classical hardware design,
but also plagued by complexity-theoretic obstacles. Motivated by fault-tolerant
quantum computation, we consider the special case of synthesizing blocks of
Clifford unitaries. Leveraging entangling input stimuli and the stabilizer
formalism allows us to reduce the Clifford synthesis problem to a family of
poly-size satisfiability (SAT) problems -- one for each target circuit depth.
On a conceptual level, our result showcases that the Clifford synthesis problem
is contained in the first level of the polynomial hierarchy ($\mathsf{NP}$),
while the classical synthesis problem for logical circuits is known to be
complete for the second level of the polynomial hierarchy
($\Sigma_2^{\mathsf{P}}$). Based on this theoretical reduction, we formulate a
SAT encoding for depth-optimal Clifford synthesis. We then employ SAT solvers
to determine a satisfying assignment or to prove that no such assignment
exists. From that, the shortest depth for which synthesis is still possible
(optimality) as well as the actual circuit (synthesis) can be obtained.
Empirical evaluations show that the optimal synthesis approach yields a
substantial depth improvement for random Clifford circuits and Clifford+T
circuits for Grover search.
