qSAT: Design of an Efficient Quantum Satisfiability Solver for Hardware Equivalence Checking

本文提出了一种用于硬件等价性检查的高效量子 SAT 求解器（qSAT），该求解器利用 Grover 算法和基于互斥积之和的 CNF 生成方法以减少量子比特需求和电路深度，并在 Qiskit 平台和 IBM 量子计算机上进行了实验验证。

要点

以下是论文《qSAT：用于硬件等价性检查的高效量子可满足性求解器设计》的通俗解释，辅以日常类比。

核心难题：大海捞针

想象你是一家玩具工厂的质量检验员。你有两个版本的复杂玩具机器人：

1. 黄金模型（$G_R$）：完美、原始的设计。
2. 测试模型（$G_I$）：从生产线上下来的新版本。

你的工作是检查它们是否完全一致。如果它们不同，你需要找出具体是哪个按钮按压或开关设置，导致新机器人做出了旧机器人不会做的动作。

在计算机芯片领域，这被称为等价性检查。传统上，我们使用“经典”计算机来解决这个问题。论文指出，对于复杂的玩具（电路），经典计算机必须逐一检查每一种可能性。如果玩具只增加几个按钮，检查所需的时间就会呈指数级增长——就像试图一颗一颗地捡起沙滩上的每一粒沙子来计数一样。对于一个 12 位乘法器（一种特定的数学芯片），论文显示，仅仅增加一个额外的位，就会让检查时间从几秒变成几小时。

解决方案：量子“超级扫描仪”

作者提出了一种名为qSAT的新工具。他们不使用经典计算机逐一检查可能性，而是利用量子计算机。

把经典计算机想象成一名侦探在黑暗的迷宫中行走，一次只检查一条路径。而量子计算机则像是一名侦探，可以神奇地分裂成千上万个克隆体，同时走遍迷宫中的每一条路径。

论文使用了一种著名的量子技巧，称为格罗弗算法（Grover's Algorithm）。想象你在电话簿中寻找一个特定的名字。

• 经典方式：你阅读第 1 页、第 2 页、第 3 页……直到找到为止。
• 量子方式（格罗弗）：你使用一种特殊的“量子放大镜”，能更快地高亮显示正确的页面。它不仅仅是快两倍，而是快平方级。如果有 100 万页，经典计算机可能需要 50 万次尝试，而量子计算机可能只需要 1000 次。

秘密武器：ESOP（“高效打包”方法）

论文最大的创新不仅仅在于使用量子计算机，而在于他们如何将问题转化为量子机器能理解的格式。

通常，将复杂的逻辑谜题翻译成量子计算机能理解的格式，就像试图把一张巨大且笨拙的沙发塞进狭小的电梯里。你需要大量的额外空间（量子比特）和大量的复杂操作（门）才能把它塞进去。

作者开发了一种名为**ESOP（异或积之和，Exclusive Sum-of-Products）**的方法。

• 类比：想象你在打包行李箱。旧方法（标准逻辑）就像把衣服随意扔进去，需要巨大的行李箱和大量的折叠。ESOP 方法则像使用真空压缩袋。它能将逻辑紧密压缩。
• 结果：这种方法需要更少的量子比特（相当于行李箱空间）和更少的门（打包所需的步骤）。论文声称，这使得量子电路呈现“线性”特征，意味着随着问题变大，其扩展性更加平滑。

“异或”电路（Miter Circuit）：比较机器

为了检查两个机器人是否相同，作者构建了一种特殊的“比较机器”，称为异或电路（Miter Circuit）。

• 他们将相同的输入同时送入黄金模型和测试模型。
• 然后他们问机器：“这两个输出匹配吗？”
• 如果机器发现差异，它会输出一个“反例”（CEX）——即一组特定的输入，证明两个机器人是不同的。

作者优化了这台比较机器。他们表明，通过使用他们的“真空压缩袋”（ESOP）方法，可以构建一个更小、更快且资源消耗更少的比较机器。

案例研究：多路复用器和全加器

为了证明他们的想法有效，他们在计算机芯片的两个常见构建模块上进行了测试：

1. 多路复用器（MUX）：一种在两个输入之间进行选择的开关。
2. 全加器：一种将三个数字相加的电路。

他们比较了构建这些电路“黄金模型”的两种方法：

• 方法 A（标准）：使用大量额外变量（就像使用 4 个额外的行李箱）。
• 方法 B（他们的 ESOP 方法）：使用更少的额外变量（就像只使用 2 个行李箱）。

结果：

• 资源更少：方法 B 使用的量子比特和门显著减少。对于全加器，他们将“格罗弗迭代”次数（量子计算机需要扫描的次数）减少了约 $\sqrt{8}$ 倍（大约快 2.8 倍）。
• 准确性：当他们在模拟器和真实的 IBM 量子计算机上运行这些测试时，“方法 B"电路更可靠（保真度更高），并且仍然以高概率（超过 75%）找到了正确答案（反例）。

总结

这篇论文提出了一种利用量子计算机检查计算机芯片是否构建正确的新方法。

1. 问题：经典计算机在检查复杂芯片时太慢了。
2. 解决方案：使用带有格罗弗算法的量子计算机来更快地搜索错误。
3. 创新：他们发明了一种新的“打包”方法（ESOP），将芯片逻辑转化为量子指令。这使得量子电路更小、更浅，运行成本更低。
4. 证明：他们在真实的芯片组件上测试了这种方法，表明它使用的资源更少，并且在当前的量子硬件上运行可靠。

本质上，他们找到了如何缩小“行李箱”的方法，让量子侦探能够挤进电梯，比以前更快地解开谜团。

技术摘要

技术摘要：qSAT——用于硬件等价性检查的高效量子可满足性求解器设计

问题陈述
硬件验证，特别是布尔电路的等价性检查，在使用经典布尔可满足性（SAT）求解器求解时，经常遭遇指数级的运行时间复杂度。尽管像 Z3（使用 SMT 和 CDCL 算法）这样的现代求解器行之有效，但它们在处理非对称结构的电路时却显得力不从心，导致随着位宽的增加，验证时间和内存需求急剧上升。本文旨在通过利用量子计算来实现对经典搜索算法的显著加速，从而满足对更高效方法的需求。

方法论
作者提出了 qSAT，这是一种专为硬件等价性检查设计的量子 SAT 求解器，利用 Grover 搜索算法。该方法建立在三个核心技术支柱之上：

1. 基于 ESOP 的子句生成：作者采用基于异或积之和（ESOP）的生成方法，而不是直接将布尔门转换为合取范式（CNF）子句——后者通常会引入昂贵的辅助变量和高昂的资源开销。通过重新定义逻辑等价关系（例如，$p \Leftrightarrow (q \lor r)$）为 ESOP 形式（例如，$p \oplus (\neg q \land \neg r)$），量子电路解释所需的量子比特数、门数和电路深度更少。
2. 量子 Miter 电路实现：验证问题被表述为一个"Miter"电路，该电路计算待测电路（$G_I$）与参考模型（$G_R$）之间的异或差异。本文详细阐述了该 Miter 的两种量子解释：
   • $V_F$：一种经济型版本，保留了辅助变量操作的结果。
   • $U_F$：一种“反计算”辅助变量的版本，将 Miter 结果严格关联到输入状态，这对于 Grover 算法中的预言机（oracle）至关重要。
     所需量子比特数估计为 $|X| + 2|A| + 1$，其中 $|X|$ 是输入变量的数量，$|A|$ 是辅助变量的数量。
3. qSAT 架构与优化：该求解器使用 $U_F$ Miter 作为 Grover 算法的预言机，以放大找到反例（CEXs）的概率。一项关键的优化策略是选择能够最小化辅助变量数量的参考模型（$G_R$）。本文展示了关于多路复用器和 1 位全加器的案例研究，表明使用 ESOP 优化的参考模型（记为 $\hat{G}_R$）与标准的基于 CNF 的参考模型相比，显著减少了所需的 Grover 迭代次数（在特定情况下减少了 $\sqrt{2^{-3}}$ 倍）。

主要贡献
本文概述了以下具体贡献：

• 架构开发：设计了一个全面的 qSAT 求解器架构，利用 Grover 搜索算法来寻找构建的 Miter 电路的解。
• 搜索空间优化：利用基于 ESOP 的子句生成和 Miter 电路实现来优化搜索空间，减少量子比特和门的开销。
• 资源评估：基于特定故障的选定基准，对 qSAT 求解器在门开销、解概率和操作保真度方面进行了评估。
• 参考模型分析：一项案例研究展示了参考电路的选择（标准型与 ESOP 优化型）如何直接影响 Grover 的迭代次数和量子资源需求。

实验结果
实验使用开源 Qiskit 平台和 IBM 量子计算机（具体为 ibm_brisbane 进行保真度分析）进行。该研究评估了注入故障的各种布尔函数（AND、NAND、OR、NOR、XOR、XNOR、MUX、CARRY 和全加器）。

• 资源效率：ESOP 优化方法（$G_F \oplus \hat{G}_R$）始终比标准方法（$G_F \oplus G_R$）需要更少的资源。例如，在全加器（FA）基准测试中，优化版本将量子比特数从 30 减少到 24，CNOT 门（#CX）从 16,413 减少到 4,941，电路深度（#D）从 26,741 减少到 7,742。
• 准确性：在理想仿真环境（Qiskit Aer）中，qSAT 求解器对优化后的 Miter 实现了 SAT 结果概率（$P(SAT) \geq 75\%$），与标准方法相当，但资源消耗显著降低。
• 保真度：在真实量子硬件上的操作保真度分析显示，与标准的 $G_R$ 模型相比，$\hat{G}_R$ 类型的参考模型在几乎所有测试的布尔函数中表现出更高的操作保真度。

意义与主张
本文声称，所提出的 qSAT 架构通过减少与 SAT 求解相关的量子资源开销（量子比特、门和深度），为高效的硬件等价性检查提供了一条可行途径。作者指出，这项工作代表了“设计完整 qSAT 求解器的首次尝试”。他们强调，该方法在数量上与被验证电路中的门数量呈线性关系，并且使用基于 ESOP 的生成方法最小化了量子电路解释的开销。结果表明，优化参考模型是使量子 SAT 求解器适用于当前及近期量子硬件的关键因素。