Provably optimal exact gate synthesis from a discrete gate set

We propose a method for exact circuit synthesis using a discrete gate set, as required for fault-tolerant quantum circuits. Our approach translates the problem of synthesizing a gate specified by its unitary matrix into a Boolean satisfiability (SAT) instance. By solving this SAT problem, we can either find a circuit that implements the target unitary or prove that no such circuit exists within a given gate count. Iterating on the gate count allows us to prove the optimality of the synthesized circuit. Our method can be further refined to account for ancillary qubits and mid-circuit measurements. Although the time-to-solution scales double-exponentially with the number of qubits, making it impractical for large circuits, many quantum algorithms rely on small, frequently used subcircuits. Finding and proving the optimal implementation of these subcircuits is essential for efficient quantum computation. In addition, proving optimality of a circuit allows to better understand circuit synthesis and eventually generalize solutions to larger circuits.