Reducing Quantum Circuit Synthesis to #SAT

TL;DR

This paper introduces a novel approach to quantum circuit synthesis by reducing it to maximum model counting (#SAT), enabling exact and approximate depth-optimal synthesis using classical #SAT tools.

Contribution

It is the first to formulate quantum circuit synthesis as a #SAT problem and extends #SAT solvers to handle quantum amplitudes for synthesis tasks.

Findings

Classical #SAT tools show potential for quantum circuit synthesis.

Extended #SAT solver d4Max supports complex and negative weights.

Experimental results demonstrate feasibility of the approach.

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.