量子电路映射的挑战

量子计算作为一种新兴计算范式，在某些问题上相比经典计算具有显著加速潜力。量子计算通常通过包含量子门的复杂电路来表示，这些门类似于传统计算机中的逻辑门。然而，当前量子硬件的电路布局相对简单，因此需要量子编译器将复杂量子计算规范映射到现有硬件。

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

基于SAT求解的创新方法

在第27届国际可满足性理论与应用会议上，我们提出了一种利用自动推理技术来寻找最小化交换门数量的电路映射新方法。可满足性问题可以表述为布尔变量和逻辑操作的表达式，求解器需要判断是否存在满足逻辑约束的变量赋值。

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

电路映射流程详解

初始量子比特布局

量子编译器首先将电路中的每个算法量子比特映射到设备的物理量子比特上。以量子傅里叶变换电路为例，该电路要求每个算法量子比特与其他两个相互作用。然而在Rigetti Aspen M-3设备的量子比特连接图中，没有形成允许两两量子比特交互的三量子比特环。

量子比特路由

初始布局后，量子傅里叶变换电路无法直接执行，这就需要通过插入量子交换门来进行量子比特路由。交换后，计算规范中针对被交换量子比特的任何门都必须重新定位到其新位置。交换门可以改变计算规范的连接要求，使其与底层量子硬件的量子比特连接性匹配。

优化框架设计

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

我们提出基于增量和并行布尔可满足性求解的新型电路映射方法。该框架通过迭代减少交换门数量并使用SAT求解器检查可行性来寻找满足电路映射要求的最小交换门数量。

给定三个输入——量子电路、量子设备和初始交换门数量，我们将量子电路映射问题编码为合取范式的SAT公式。SAT求解器以CNF作为输入并检查其可满足性。可满足的结果表明存在使用不超过S个交换门的有效映射。在这种情况下，我们减少交换门数量S并继续循环以寻找使用更少交换门的映射。当求解器返回不可满足时退出循环，最后从已获得的最佳结果解码映射电路。

我们开发了高效实现来解决编码的电路映射问题：使用增量SAT编码迭代减少交换门数量S，无需在每次迭代时重新编码整个问题；设计定制求解器利用并行求解技术提高增量求解性能。

实验结果

对真实量子算法和设备进行全面评估表明，我们的方法比现有基于求解器的方法快26倍，并产生更好的结果。在76%的实例上改进了启发式方法，平均减少26%的交换门数量。

实验结果显示，新方法在Rigetti Aspen M-3设备上运行量子傅里叶变换算法时，相比传统方法显著减少了交换操作数量和运行时间，为量子计算的实际应用提供了更高效的编译方案。