量子电路合成任务旨在将给定量子算子分解为基本量子门序列。由于有限目标门集无法精确实现任意算子，近似实现通常不可避免。模型计数（#SAT）作为一种新兴方法，近期被证实可有效解决量子电路分析中的核心问题。该工作首次证明普适量子电路合成问题可归约为最大模型计数问题，并构建了面向Clifford+T门集的精确与近似深度最优量子电路合成的#SAT编码方案。研究人员通过开源实现评估该方法，采用最大模型计数器d4Max作为后端引擎，并扩展了d4Max对复振幅与负权值的支持。实验结果表明，现有经典工具在量子电路合成领域具有应用潜力。
