Finding optimal fault-tolerant circuits via satisfiability modulo theory

Traditional fault tolerant schemes such as Shor, Steane, and Knill type error correction have large qubit overhead and there are efforts in reducing overhead with scheme such as adding flag qubits. To find the optimal circuit in terms of qubit count, circuit depth, and two-qubit gate count, we compactly encode the fault-tolerant constraints using the circuit to code mapping and find error correction conditions on the spacetime code that satisfy the fault-tolerant conditions for distance three codes. We are able to prove optimality of syndrome extraction and state preparation circuits via satisfiability modulo theory (SMT) solver for some small codes with a given gate set and show improvements on other protocols via Monte Carlo simulation.