Reducing Quantum Circuit Synthesis to #SAT
Dekel Zak, Jingyi Mei, Jean-Marie Lagniez, Alfons Laarman
TL;DR
The paper tackles the challenge of synthesizing quantum circuits within a finite gate set by reducing universal circuit synthesis to maximum weighted model counting (MWMC). It introduces two encodings, computational basis (CB) and Pauli basis (PB), enabling exact and approximate depth-optimal synthesis for Clifford+T circuits through a single MWMC call per equivalence check and fidelity evaluation. An open-source tool, Quokka#-syn, demonstrates the approach, extending MWMC solvers to handle complex and negative weights and providing layer-based synthesis with pruning rules. While results show the approach is promising and competitive with existing methods in certain regimes, scalability remains a key challenge, guiding future work toward incremental solving, solver enhancements, symmetry exploitation, and broader gate-set applicability.
Abstract
Quantum circuit synthesis is the task of decomposing a given quantum operator into a sequence of elementary quantum gates. Since the finite target gate set cannot exactly implement any given operator, approximation is often necessary. Model counting, or #SAT, has recently been demonstrated as a promising new approach for tackling core problems in quantum circuit analysis. In this work, we show for the first time that the universal quantum circuit synthesis problem can be reduced to maximum model counting. We formulate a #SAT encoding for exact and approximate depth-optimal quantum circuit synthesis into the Clifford+T gate set. We evaluate our method with an open-source implementation that uses the maximum model counter d4Max as a backend. For this purpose, we extended d4Max with support for complex and negative weights to represent amplitudes. Experimental results show that existing classical tools have potential for the quantum circuit synthesis problem.