基于SAT求解的量子电路映射优化技术

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

在涉及真实量子设备和算法的实验中，这种基于自动推理的量子计算映射方法比现有技术快26倍。

量子计算(QC)是一种新的计算范式，有望在某些问题上实现相对于经典计算的显著加速。量子计算通常表示为涉及量子"门"的复杂电路，这些门类似于传统计算机中的逻辑门。然而，构建量子计算机的困难意味着当前量子硬件可用的电路布局相对简单。量子编译器是将量子计算规范的复杂电路映射到当今可用较简单电路的程序。

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

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

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

电路映射

就像逻辑门是经典计算的基本构建块一样，量子门是量子计算的基本构建块。但量子门操作涉及以某种方式操纵量子系统(例如改变其磁场)，因此与常规逻辑门不同，量子门在特定时间点应用。交换门是基本量子门之一；其他包括使量子位进入叠加态(不同可能状态的混合)的Hadamard门和旋转门。

我们通过一个例子说明量子电路映射问题。下图左侧示意图表示Rigetti Aspen M-3量子计算机(部分)的量子位连接性。圆圈代表物理量子位，线条代表允许应用双量子位门的物理链接。

右侧是著名量子傅里叶变换(QFT)算法的三量子位量子电路图。三条水平线表示三个算法量子位上的量子门时间安排。标有H的方框表示单量子位Hadamard门，标有R并连接到实心点的方框表示双量子位受控旋转门。QFT电路在三个量子位中每两个量子位子集之间都有一个双量子位旋转门。

在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%的交换门数量。