量子计算（QC）作为一种新兴计算范式，有望在特定问题上实现超越经典计算的加速。量子计算通常表示为包含量子"门"的复杂电路，这些门类似于传统计算机中的逻辑门。然而，由于量子计算机构建难度大，当前量子硬件的电路布局相对简单。量子编译器的作用就是将量子计算规范的复杂电路映射到现有的简单电路上。

电路映射过程大量使用交换门（swap gate），该门可以交换两个相邻量子比特（qubit）的状态。通过一次或多次交换，量子比特状态可以在电路中移动，直至与需要交互的下一个量子比特相邻。但交换门成本高且易出错，编译器应尽量减少其使用。

在第二十七届国际可满足性理论及应用会议（SAT）上发表的论文中，提出了一种利用自动推理寻找最小化交换门数量的电路映射新方法。可满足性（SAT）问题可表述为布尔（二进制）变量和逻辑运算的表达式，核心问题是是否存在满足表达式逻辑约束的变量赋值。在该方法中，交换门数量限制就是必须满足的约束条件之一，SAT求解器会判断该条件是否可满足。

通过对各类量子设备和算法的实际案例进行全面评估，该方法比最先进的基于求解器的方法快26倍，将重要量子应用的编译时间从数小时缩短至几分钟。与当前启发式算法相比，该方法平均减少26%的交换门数量。这是某机构自动推理组与量子团队（某量子平台）的合作项目。

电路映射原理 与传统计算以逻辑门为基本构建模块类似，量子门是量子计算的基础构建模块。但量子门操作涉及对量子系统的特定操控（如改变磁场），因此与常规逻辑门不同，量子门需要在特定时间点施加。交换门是基本量子门之一，其他还包括使量子比特进入叠加态（多种可能状态的混合）的Hadamard门，以及旋转门等。

通过一个示例说明量子电路映射问题：左侧示意图表示（部分）Rigetti Aspen M-3量子计算机的量子比特连接性，圆圈代表物理量子比特，连线表示允许施加双量子比特门的物理链接；右侧是著名量子傅里叶变换（QFT）算法的三量子比特电路图，三条水平线表示三个算法量子比特上的量子门时间调度，标有H的方框表示单量子比特Hadamard门，标有R并连接实心点的方框表示双量子比特受控旋转门。

在Aspen M-3设备上执行QFT电路需要量子编译器进行电路映射，该过程包含两个步骤：初始量子比特布局和量子比特路由。初始布局阶段，量子编译器将电路中每个算法量子比特映射到设备的物理量子比特上。由于QFT电路要求每个算法量子比特都与其他两个交互，而Aspen M-3的量子比特连接图中不存在允许两两交互的三量子比特环结构，因此初始布局后QFT电路无法直接执行，这就需要进行第二步：量子比特路由。

量子比特路由通过插入量子交换门实现。交换后，计算规范中针对被交换量子比特的门必须重新定位到新位置。从示例可见，交换门可以改变计算规范的连接需求，使其与底层量子硬件的量子比特连接性匹配。

优化方法 当前电路映射问题主要有两种解决途径：基于求解器的算法和基于启发式的算法。前者能获得最优交换门数量但编译时间长；后者速度快但交换门数量通常次优。我们提出基于布尔可满足性（SAT）增量式并行求解的新型电路映射方法。

该方法框架如下：通过迭代减少交换门数量（S）并用SAT求解器检查可行性，寻找满足电路映射要求的最小交换门数量。给定三个输入——量子电路、量子设备（QPU）和初始交换门数量（S），我们将量子电路映射问题编码为合取范式（CNF）的SAT公式。SAT求解器以CNF为输入并检查其可满足性。可满足（SAT）结果表示存在使用不超过S个交换门的有效映射，此时我们减少S并继续循环搜索使用更少交换门的映射。当求解器返回不可满足（UNSAT）时退出循环，表示无法进一步减少交换门数量。最后，我们从目前获得的最佳结果解码出映射电路。

我们开发了高效实现方案来解决编码后的电路映射问题：使用增量式SAT编码迭代减少交换门数量S，无需每次迭代重新编码整个问题，使求解器能复用之前迭代的内部状态以减少总运行时间；还设计了定制求解器利用并行求解技术提升增量式求解性能。

对真实量子算法和设备的全面评估表明，该方法比现有基于求解器的方法快26倍且结果更优。在76%的案例中，该方法也优于启发式方法，平均减少26%的交换门数量。实验结果表格对比了新型基于SAT的电路映射方法（SATmapper）与两种前代方法在交换操作数量和运行时间上的表现。