标题： 将量子电路综合问题转化为#SAT 显示英文标题

标题： Reducing Quantum Circuit Synthesis to #SAT

摘要： 量子电路综合的任务是将给定的量子算子分解为一系列基本的量子门序列。 由于有限的目标门集无法精确实现任何给定的算子，因此通常需要进行近似。 模型计数，或#SAT，最近被证明是解决量子电路分析中核心问题的一种有前景的新方法。 在本工作中，我们首次表明，通用量子电路综合问题可以归约到最大模型计数。 我们将精确和近似的深度最优量子电路综合问题编码为#SAT，以进入Clifford+T门集。 我们使用一个开源实现来评估我们的方法，该实现以最大模型计数器d4Max作为后端。 为此，我们扩展了d4Max，以支持复数和负权重来表示振幅。 实验结果表明，现有的经典工具在量子电路综合问题上具有潜力。 显示英文摘要

摘要： 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.