利用SAT求解优化量子电路映射

量子计算(QC)作为一种新兴计算范式，有望在特定问题上实现相对于经典计算的显著加速。量子计算通常表示为包含量子“门”的复杂电路，这些门类似于传统计算机中的逻辑门。然而，量子计算机的构建难度导致当前量子硬件仅能提供相对简单的电路布局。量子编译器的作用就是将量子计算规范中的复杂电路映射到当前可用的简化电路上。

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

在第27届国际可满足性理论及应用会议(SAT)上发表的论文中，提出了一种利用自动推理寻找最小化交换门数量的电路映射新方法。可满足性(SAT)问题可表述为布尔(二进制)变量和逻辑运算的表达式，其核心是判断是否存在满足表达式逻辑约束的变量赋值方案。

在该方法中，交换门数量限制是必须满足的约束条件之一，SAT求解器会判断该条件是否可满足。通过对多种量子设备和算法的实际实例进行全面评估，该方法比最先进的基于求解器的方法快26倍，将重要量子应用的编译时间从数小时缩短至数分钟。与当前启发式算法相比，该方法平均减少26%的交换门数量。

电路映射原理

量子门是量子计算的基本构建模块，类似于经典计算中的逻辑门。但量子门操作涉及对量子系统的特定操控（如改变磁场），因此需要在特定时间点施加。交换门是基本量子门之一，其他还包括使量子比特进入叠加态（不同可能状态的混合）的Hadamard门和旋转门。

通过具体示例说明量子电路映射问题：左图展示Rigetti Aspen M-3量子计算机的量子比特连接图（圆圈代表物理量子比特，连线代表允许双量子比特门操作的物理链接）；右图是著名量子傅里叶变换(QFT)算法的三量子比特电路图。水平线表示三个算法量子比特上量子门的时间调度，H标签框表示单量子比特Hadamard门，R标签框与实心点连接表示双量子比特受控旋转门。

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

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

优化方法

当前电路映射问题主要有基于求解器和启发式算法两种方法，但各有缺陷：基于求解器的方法能获得最优交换门数量但编译时间长；启发式算法速度快但交换门数量通常次优。

提出的新方法基于增量和并行布尔可满足性(SAT)求解技术。其框架通过迭代减少交换门数量(S)并使用SAT求解器检查可行性，以寻找满足电路映射要求的最小交换门数量。

给定量子电路、量子设备(QPU)和初始交换门数量(S)三个输入，将量子电路映射问题编码为合取范式(CNF)的SAT公式。SAT求解器以CNF为输入检查可满足性：可满足(SAT)结果表示存在使用不超过S个交换门的有效映射，此时减少S值继续循环搜索；当求解器返回不可满足(UNSAT)时退出循环，表示无法进一步减少交换门数量。最后从获得的最佳结果解码映射后的电路。

开发了高效实现方案：使用增量SAT编码迭代减少S值，无需每次迭代重新编码整个问题，使求解器能复用之前迭代的内部状态降低总运行时间；还设计了定制求解器利用并行求解技术提升增量求解性能。

实验结果

对真实量子算法和设备的综合评估表明，新方法比现有基于求解器的方法快26倍且结果更优。在76%的实例中超越启发式方法，平均实现26%的交换门数量减少。

实验结果显示：在Rigetti-AspenM-3_3q-QFT实例中，新方法仅需2个交换操作，耗时0.1秒；而传统求解器方法需3个交换操作耗时2.6秒，启发式方法需3个交换操作耗时0.01秒。在IBM-Tokyo_5q-QFT实例中，新方法以4个交换操作（0.4秒）优于求解器方法的5个交换操作（10.5秒）和启发式方法的5个交换操作（0.02秒）。

该方法由某中心自动推理组与量子团队联合开发，相关研究成果已提交SAT 2024最佳学生论文奖评选并获得亚军。