2026-09-17T02:11:37Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:23899 2026-09-05T18:28:17Z ddc:004 open_access

Reducing Quantum Circuit Synthesis to #SAT Zak, Dekel Mei, Jingyi Lagniez, Jean-Marie Laarman, Alfons Maximum weighted model counting quantum circuit synthesis 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dekel Zak and Jingyi Mei and Jean-Marie Lagniez and Alfons Laarman 2025 Is Part Of LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CP.2025.38 urn:nbn:de:0030-drops-238997 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.38 eng https://creativecommons.org/licenses/by/4.0/legalcode