在内存计算中本地加速混合 XOR–CNF 布尔可满足性问题

为何更快的问题求解至关重要

许多影响我们日常生活的任务——从保障在线通信到设计更快的电子设备——都归结为向计算机提出一个是或否的问题：是否存在一组开关的组合能使这个庞大的逻辑规则为真？这就是布尔可满足性问题（SAT）。SAT 问题以其困难著称，随着这些任务规模和重要性的增加，求解它们所需的时间和能量成为主要瓶颈。本文探讨了一种通过同时重构数学表达和硬件设计，使二者在一种特殊类型的存储芯片内协同工作的全新途径，以加速 SAT 求解。

将纠结的规则化为更简单的构件

传统 SAT 求解器通常使用一种由“或”（OR）条件构成的逻辑描述来表达问题。但许多现实的工业问题——例如解码无线信号、检测芯片故障或攻破某些密码方案——天然地将“或”（OR）与“异或”（XOR）混合使用，后者是一种当任一输入翻转时会变动的奇偶校验。现有工具常常被迫将这些 XOR 规则改写成仅用 OR 表示的形式，这会膨胀问题规模并拖慢求解速度。作者选择保留两类规则，构建一种混合描述，更贴近问题在实践中出现的形式。

用更少的部件完成更多工作

研究人员将这种混合描述与传统描述在多个基准族上进行了仔细比较，这些基准来自密码学领域和一个称为最小不一致奇偶校验的经典测试问题。通过自动重建隐藏的 XOR 结构并首先应用智能化简，他们表明，混合表示能够将变量数量缩减数倍，并将规则数量大致减少四到五倍。换言之，当允许 XOR 与 OR 共存时，同样的逻辑问题常常可以用远少得多的要素来表述。更小的问题不仅对软件更友好，也便于那些在可同时存储规则数量上有严格限制的专用硬件处理。

让存储芯片来做“思考”工作

为利用这一更精简的描述，团队设计了专用的“内存计算”加速器。该装置不再在处理器和存储器之间频繁搬运数据，而是在数据所在的位置——由称作忆阻器的微小电子元件构成的格子内——执行大部分计算。他们将一种已知的局部搜索策略 WalkSAT 改造为原生支持 XOR–OR 混合规则的新变体 WalkSAT-XNF。算法的每一步——检查哪些规则被违反、估计每个开关的重要性、加入少量噪声以跳出死胡同，以及翻转最佳候选——都直接在交叉阵列的模拟电路中实现，简单的辅助电路负责选择下一个要翻转的变量。

在实验室与仿真中验证其有效性

作者首先构建了一个小型原型，使用忆阻器芯片证明模拟硬件即便在制造差异和电气噪声存在时，也能忠实地评估子句并指导搜索。对适中规模测试实例的实验显示，硬件行为与理想仿真非常接近。随后他们对更先进的 28 纳米设计进行了建模，并在密码学与奇偶校验问题族上进行了基准测试。由于混合描述在更少的子句中承载了更多信息，加速器所需的片上存储显著减少，且每一步的能耗大幅低于仅支持 OR 的版本。总体而言，与在通用 CPU 上运行的领先软件 SAT 求解器相比，混合内存求解器在速度上大约实现十倍加速，能效上约提升千倍。

这对未来计算机意味着什么

简单来说，这项工作表明，通过将逻辑规则的书写方式与一种新型基于内存的硬件的计算方式相匹配，我们可以用更少的能量、更高的速度求解某些著名的困难是/否问题。通过在芯片内原生支持 XOR 与 OR 规则，所提出的加速器可以用更小、更冷、更快的硬件处理现实的密码学、通信和电路设计任务。随着计算系统越来越接近能耗和速度的极限，这类面向特定问题的内存内计算方法可能有助于保持关键数字基础设施的安全与高效。

引用: Im, H., Böhm, F., Pedretti, G. et al. Accelerating hybrid XOR–CNF Boolean satisfiability problems natively with in-memory computing. Nat Commun 17, 2922 (2026). https://doi.org/10.1038/s41467-026-69465-2

关键词: 布尔可满足性, 内存计算, 忆阻交叉阵列, 硬件加速器, 密码学