基于多值阻变存储器与子句折叠策略的并行梯度布尔可满足性求解器

岳文硕; 叶林韬; 史代璟; 符一涵; 杨宇翔; 赵洪霄; 李嘉怡; 张腾; 燕博南; 杨玉超

doi:10.12263/DZXB.20250966

您当前的位置：

首页 >

文章列表页 >

基于多值阻变存储器与子句折叠策略的并行梯度布尔可满足性求解器

面向高效人工智能的新型架构与电子系统 | 更新时间：2026-10-16

- 基于多值阻变存储器与子句折叠策略的并行梯度布尔可满足性求解器
- Multilevel Resistive Memory Enabled Parallel-Gradient Boolean Satisfiability Solver with Clause-Folding Scheme
- 电子学报 2026年54卷第6期页码：2403-2414
- 作者机构：
  
  1.北京大学集成电路学院/集成电路高精尖创新中心新基石科学实验室，北京 100871
  2.北京大学人工智能研究院，北京 100871
  3.北京大学信息科学技术学院，北京 100871
  4.北京大学信息工程学院广东省存算一体芯片重点实验室新基石科学实验室，广东深圳 518055
  5.北京脑科学与类脑研究所，北京 102206
- 作者简介：
  
  岳文硕男，1999年1月出生于北京市。2021年于北京大学获得学士学位，现为北京大学集成电路学院博士研究生。主要研究方向为忆阻器存内计算。中国电子学会会员编号：E190203508M。E-mail: yws2017@pku.edu.cn
  叶林韬男，2003年8月出生于北京市。2025年毕业于北京大学信息科学技术学院，现为美国南加州大学博士研究生。主要研究方向为新型存储芯片。E-mail: lintaoye@pku.edu.cn
  史代璟男，1999年12月出生于福建省三明市。现为北京大学集成电路学院博士研究生。主要研究方向为存内计算外围电路设计。E-mail: daijingshi@pku.edu.cn
  符一涵男，2000年10月出生于江苏省丹阳市。2023年于北京大学获得学士学位，现为北京大学人工智能研究院博士研究生。主要研究方向为计算机体系结构与人工智能加速器。E-mail: yihanfu@pku.edu.cn
  杨宇翔男，2001年2月出生于广东省梅州市。现为北京大学集成电路学院博士研究生。主要研究方向为忆阻器及其应用。中国电子学会会员编号：E190034611A。E-mail: yangyuxiang@pku.edu.cn
  赵洪霄男，2001年12月出生于江苏省宿迁市。现为北京大学人工智能研究院博士研究生。主要研究方向为认知架构及其应用。E-mail: hongxiaozhao@stu.pku.edu.cn
  李嘉怡女，2001年3月出生于山西省运城市。现为北京大学人工智能研究院博士研究生。主要研究方向为强化学习的硬件加速及片间互联系统。E-mail: lijiayi@stu.pku.edu.cn
  张腾男，1994年10月出生于安徽省芜湖市。现为北京大学助理研究员。主要研究方向为后摩尔器件集成、感存算一体。E-mail: tengzhang@pku.edu.cn
  燕博南男，1991年6月出生于河北省保定市。现为北京大学人工智能研究院助理教授，北京大学小米博雅青年学者，博士生导师，北京大学通用人工智能芯片研究中心执行主任。主要研究方向为通用人工智能体处理器芯片设计、SRAM与新兴存储器（MRAM、RRAM、PCM、FeFET等）集成电路设计。E-mail: bonanyan@pku.edu.cn
  杨玉超男，1984年12月出生于河北省衡水市。现为北京大学博雅特聘教授，国家杰青，新基石研究员，信息工程学院院长，科学智能学院副院长。主要研究方向为存算一体芯片、类脑计算、脑机接口等。中国电子学会会员编号：E190014285S。E-mail: yuchaoyang@pku.edu.cn
- 基金信息：
  
  国家重点研发计划(2023YFB4502200);国家自然科学基金(92164302;92364102;T2350006);广东省存算一体芯片重点实验室(2024B1212020002);北京市自然科学基金(L234026;L257010);高等学校学科创新引智计划（111计划）(B18001);新基石科学基金会的资助
- DOI：10.12263/DZXB.20250966
  中图分类号： TP302.1;TP389.1
- 收稿：2025-11-27，
  
  录用：2025-12-22，
  
  纸质出版：2026-06-25
- 稿件说明：
移动端阅览
岳文硕, 叶林韬, 史代璟, 等. 基于多值阻变存储器与子句折叠策略的并行梯度布尔可满足性求解器[J]. 电子学报, 2026, 54(06): 2403-2414.

YUE Wenshuo, YE Lintao, SHI Daijing, et al. Multilevel Resistive Memory Enabled Parallel-Gradient Boolean Satisfiability Solver with Clause-Folding Scheme[J]. Acta Electronica Sinica, 2026, 54(06): 2403-2414.
岳文硕, 叶林韬, 史代璟, 等. 基于多值阻变存储器与子句折叠策略的并行梯度布尔可满足性求解器[J]. 电子学报, 2026, 54(06): 2403-2414. DOI：10.12263/DZXB.20250966

YUE Wenshuo, YE Lintao, SHI Daijing, et al. Multilevel Resistive Memory Enabled Parallel-Gradient Boolean Satisfiability Solver with Clause-Folding Scheme[J]. Acta Electronica Sinica, 2026, 54(06): 2403-2414. DOI：10.12263/DZXB.20250966

摘要

本研究提出了一种基于存内计算技术和多值阻变存储器的并行梯度硬件布尔可满足性求解器——Fold-SAT。如其名称所示，Fold-SAT将多个子句折叠存储到存内计算阵列的单个列中，即子句折叠策略。存内计算可以利用其高计算并行度对可满足性问题求解进行硬件加速。传统的存内可满足性求解器每列仅存储一个子句，其存储阵列稀疏度较高，常常占用较大存储空间。在迭代过程中，存内计算加速器通过阵列上的乘累加计算实现对子句可满足性的计算。本工作通过多电阻态表征不同子句的结构信息，可以在阵列中使用一列存储多个子句的信息，并在读出阶段解码得到各个子句对应的可满足性结果。并行梯度计算是一种面向可满足性求解的高效算法，其前向传播阵列与反向传播阵列均可使用子句折叠策略进行压缩。为了探究子句折叠策略对于可满足性问题的压缩存储效果，本研究面向并行梯度计算设计了阵列中多值存储的电阻比例并研究其对数据压缩的影响。结果表明，当前向传播阵列采用1∶4∶16的电阻态比例时，该方法能将存储阵列规模缩小至传统方案的1/3，并将总体存储稀疏度从97.0%降低至约92.8%，其中存储稀疏度定义为阵列中不存储有效信息的单元占比。此外，本研究还开发了在反向传播阵列中的数据压缩方案，通过多值映射可以将反向传播阵列所需阵列规模缩小至传统方案的1/2。本研究探讨了器件非理想效应及参数设计所带来的影响，仿真结果表明，器件编程与读出需要将器件偏差控制在1 μS以内，电导均值偏移需要控制在基准值的10%以内。而反向传播阵列中的多值器件具有一系列可选择范围，多值器件范围在1∶8~1∶16之间均可实现合理的计算精度。仿真结果显示，本工作

=50的问题平均求解时间约为19.74 μs，与当前领先的加速器速度接近，说明本工作可以在保持较高的计算速度同时缩小其所需存储器阵列规模。

Abstract

This work introduces a hardware parallel-gradient boolean satisfiability solver

Fold-SAT

enabled by compute-in-memory technology and multilevel resistive memory storage. As shown in its name

Fold-SAT folds multiple clauses into one column of the compute-in-memory array. Compute-in-memory can utilize its computing parallelism to accelerate the solving process of satisfiability problems on hardware. A conventional in-memory SAT-solver only stores one clause per column. It shows high sparsity when stored in memory and usually occupies large memory capacity. During computing iterations

the compute-in-memory accelerator conducts multiply-and-accumulate operations on the array to calculate the satisfiability result of each clause. Fold-SAT uses multiple resistance states to represent the structural information of different clauses. It stores the information of multiple clauses in each column and decodes the satisfiability results of the clauses during readout process. Parallel gradient algorithm is an efficient algorithm for satisfiability problems. The clause-folding scheme applies to both the forward-pass array and the backward-path array in parallel gradient algorithm. To explore the compression result of Fold-SAT

this work designs the resistance ratio of multilevel storage and examines its effects on data compression. Results reveal that

when the forward-pass array uses a resistance ratio of 1:4:16

it reduces the array size to 1/3 of conventional methods and reduces the overall storage sparsity from 97.0% to about 92.8%. The storage sparsity refers to the portion of cells that do not store effective information. Moreover

this work explores the data compression in the backward-pass array. It reduces the required array size to half that of conventional methods. This work discusses the impacts of device non-idealities. Simulated results show that the device-programming algorithms should reduce the device errors to less than 1 μS

and the deviation of conductance mean values should be controlled within 10%. There is a series of design spaces regarding the multilevel devices for the backward-pass array. It could reach acceptable computing precision when the resistance ratio is set between 1:8 to 1:16 for the backward-pass array. Simulation results show that this work achieves a median solving time of 19.74 μs

which is close to the leading work in the literature. This illustrates that this work could reduce the memory capacity cost while maintaining comparatively high solving speed.

关键词

Keywords

references

Biere A , Heule M , van Maaren H , et al . Handbook of satisfiability: Part 1/Part 2 [M ] . 2nd ed . Amsterdam : IOS Press , 2021 . DOI: 10.3233/faia336 http://dx.doi.org/10.3233/faia336

Schaefer T J . The complexity of satisfiability problems [C ] // Proceedings of the Tenth Annual ACM Symposium on Theory of Computing . San Diego : ACM , 1978 : 216 - 226 . DOI: 10.1145/800133.804350 http://dx.doi.org/10.1145/800133.804350

Marques-Silva J . Practical applications of Boolean satisfiability [C ] // 2008 9th International Workshop on Discrete Event Systems . Gothenburg : IEEE , 2008 : 74 - 80 . DOI: 10.1109/WODES.2008.4605925 http://dx.doi.org/10.1109/WODES.2008.4605925

Ganai M K , Gupta A . SAT-based scalable formal verification solutions [M ] . New York : Springer , 2007 . DOI: 10.1007/978-0-387-69167-1 http://dx.doi.org/10.1007/978-0-387-69167-1

Prasad M R , Biere A , Gupta A . A survey of recent advances in SAT-based formal verification [J ] . International Journal on Software Tools for Technology Transfer , 2005 , 7 ( 2 ): 156 - 173 . DOI: 10.1007/s10009-004-0183-4 http://dx.doi.org/10.1007/s10009-004-0183-4

Marques-Silva J P , Sakallah K A . Boolean satisfiability in electronic design automation [C ] // Proceedings of the 37th Annual Design Automation Conference . Los Angeles : ACM , 2000 : 675 - 680 . DOI: 10.1145/337292.337611 http://dx.doi.org/10.1145/337292.337611

Li Min , Shi Zhengyuan , Lai Qiuxia , et al . On EDA-driven learning for SAT solving [C ] // 2023 60th ACM/IEEE Design Automation Conference . San Francisco : IEEE , 2023 : 10248001 . DOI: 10.1109/dac56929.2023.10248001 http://dx.doi.org/10.1109/dac56929.2023.10248001

Martins R , Manquinho V , Lynce I . An overview of parallel SAT solving [J ] . Constraints , 2012 , 17 ( 3 ): 304 - 347 . DOI: 10.1007/s10601-012-9121-3 http://dx.doi.org/10.1007/s10601-012-9121-3

Goldberg E , Novikov Y . BerkMin: A fast and robust sat-solver [J ] . Discrete Applied Mathematics , 2007 , 155 ( 12 ): 1549 - 1561 . DOI: 10.1016/j.dam.2006.10.007 http://dx.doi.org/10.1016/j.dam.2006.10.007

Xie Shanshan , Yang Mengtian , Lanham S A , et al . 29.2 snap-SAT: A one-shot energy-performance-aware all-digital compute-in-memory solver for large-scale hard Boolean satisfiability problems [C ] // 2023 IEEE International Solid-State Circuits Conference . San Francisco : IEEE , 2023 : 420 - 422 . DOI: 10.1109/isscc42615.2023.10067380 http://dx.doi.org/10.1109/isscc42615.2023.10067380

Shim C , Bae J , Kim B . 30.3 VIP-Sat: A Boolean satisfiability solver featuring 5×12 variable in-memory processing elements with 98% solvability for 50-variables 218-clauses 3-SAT problems [C ] // 2024 IEEE International Solid-State Circuits Conference . San Francisco : IEEE , 2024 : 486 - 488 . DOI: 10.1109/isscc49657.2024.10454397 http://dx.doi.org/10.1109/isscc49657.2024.10454397

Kim D , Rahman N M , Mukhopadhyay S . 29.1~32.5 mW mixed-signal processing-in-memory-based k-SAT solver in 65 nm CMOS with 74.0% solvability for 30-variable 126-clause 3-SAT problems [C ] // 2023 IEEE International Solid-State Circuits Conference . San Francisco : IEEE , 2023 : 28 - 30 . DOI: 10.1109/isscc42615.2023.10067570 http://dx.doi.org/10.1109/isscc42615.2023.10067570

Bhattacharya T , Hutchinson G H , Pedretti G , et al . Computing high-degree polynomial gradients in memory [J ] . Nature Communications , 2024 , 15 ( 1 ): 8211 . DOI: 10.1038/s41467-024-52488-y http://dx.doi.org/10.1038/s41467-024-52488-y

Sohanghpurwala A A , Hassan M W , Athanas P . Hardware accelerated SAT solvers: A survey [J ] . Journal of Parallel and Distributed Computing , 2017 , 106 : 170 - 184 . DOI: 10.1016/j.jpdc.2016.12.014 http://dx.doi.org/10.1016/j.jpdc.2016.12.014

Ivan T , Aboulhamid E M . An efficient hardware implementation of a SAT problem solver on FPGA [C ] // 2013 Euromicro Conference on Digital System Design . Los Alamitos : IEEE , 2013 : 209 - 216 . DOI: 10.1109/dsd.2013.31 http://dx.doi.org/10.1109/dsd.2013.31

Nguyen A H N , Aono M , Hara-Azumi Y . FPGA-based hardware/software co-design of a bio-inspired SAT solver [J ] . IEEE Access , 2020 , 8 : 49053 - 49065 . DOI: 10.1109/access.2020.2980008 http://dx.doi.org/10.1109/access.2020.2980008

Zhang Qiaochu , Su Shiyu , Liu Zerui , et al . A stochastic analog SAT solver in 65 nm CMOS achieving 6.6 μs average solution time with 100% solvability for hard 3-SAT problems [C ] // 2024 IEEE Symposium on VLSI Technology and Circuits (VLSI Technology and Circuits) . Honolulu : IEEE , 2024 : 1 - 2 . DOI: 10.1109/vlsitechnologyandcir46783.2024.10631503 http://dx.doi.org/10.1109/vlsitechnologyandcir46783.2024.10631503

Yan Bonan , Hsu J L , Yu P C , et al . A 1.041-mb/mm 2 27.38-TOPS/W signed-INT8 dynamic-logic-based ADC-less SRAM compute-in-memory macro in 28 nm with reconfigurable bitwise operation for AI and embedded applications [C ] // 2022 IEEE International Solid-State Circuits Conference . San Francisco : IEEE , 2022 : 188 - 190 . DOI: 10.1109/isscc42614.2022.9731545 http://dx.doi.org/10.1109/isscc42614.2022.9731545

Verma N , Jia Hongyang , Valavi H , et al . In-memory computing: Advances and prospects [J ] . IEEE Solid-State Circuits Magazine , 2019 , 11 ( 3 ): 43 - 55 . DOI: 10.1109/mssc.2019.2922889 http://dx.doi.org/10.1109/mssc.2019.2922889

Wan Weier , Kubendran R , Schaefer C , et al . A compute-in-memory chip based on resistive random-access memory [J ] . Nature , 2022 , 608 ( 7923 ): 504 - 512 . DOI: 10.1038/s41586-022-04992-8 http://dx.doi.org/10.1038/s41586-022-04992-8

李嘉宁 , 姚鹏 , 揭路 , 等 . 存算一体技术研究现状 [J ] . 电子学报 , 2024 , 52 ( 4 ): 1103 - 1117 . DOI: 10.12263/DZXB.20230967 http://dx.doi.org/10.12263/DZXB.20230967

Li Jianing , Yao Peng , Jie Lu , et al . Research status of computing-in-memory technology [J ] . Acta Electronica Sinica , 2024 , 52 ( 4 ): 1103 - 1117 . (in Chinese) . DOI: 10.12263/DZXB.20230967 http://dx.doi.org/10.12263/DZXB.20230967

Li Wantong , Sun Xiaoyu , Huang Shanshi , et al . A 40-nm MLC-RRAM compute-in-memory macro with sparsity control, on-chip write-verify, and temperature-independent ADC references [J ] . IEEE Journal of Solid-State Circuits , 2022 , 57 ( 9 ): 2868 - 2877 . DOI: 10.1109/jssc.2022.3163197 http://dx.doi.org/10.1109/jssc.2022.3163197

Park J , Kumar A , Zhou Yucheng , et al . Multi-level, forming and filament free, bulk switching trilayer RRAM for neuromorphic computing at the edge [J ] . Nature Communications , 2024 , 15 ( 1 ): 3492 . DOI: 10.1038/s41467-024-46682-1 http://dx.doi.org/10.1038/s41467-024-46682-1

Wu Wei , Wu Huaqiang , Gao Bin , et al . A methodology to improve linearity of analog RRAM for neuromorphic computing [C ] // 2018 IEEE Symposium on VLSI Technology . Honolulu : IEEE , 2018 : 103 - 104 . DOI: 10.1109/VLSIT.2018.8510690 http://dx.doi.org/10.1109/VLSIT.2018.8510690

Du Yiwei , Tang Jianshi , Li Yijun , et al . Monolithic 3D integration of analog RRAM-based computing-in-memory and sensor for energy-efficient near-sensor computing [J ] . Advanced Materials , 2024 , 36 ( 22 ): 2470164 . DOI: 10.1002/adma.202470164 http://dx.doi.org/10.1002/adma.202470164

Song Wenhao , Rao Mingyi , Li Yunning , et al . Programming memristor arrays with arbitrarily high precision for analog computing [J ] . Science , 2024 , 383 ( 6685 ): 903 - 910 . DOI: 10.1126/science.adi9405 http://dx.doi.org/10.1126/science.adi9405

Rao Mingyi , Tang Hao , Wu Jiangbin , et al . Thousands of conductance levels in memristors integrated on CMOS [J ] . Nature , 2023 , 615 ( 7954 ): 823 - 829 . DOI: 10.1038/s41586-023-05759-5 http://dx.doi.org/10.1038/s41586-023-05759-5

Jo Y J , Yap B P , Yoon D H , et al . DenseCIM: Binary weighted-capacitor SRAM computation-In-memory with column-by-column dynamic range calibration SAR ADC [C ] // 2023 IEEE Custom Integrated Circuits Conference . San Antonio : IEEE , 2023 : 10121213 . DOI: 10.1109/cicc57935.2023.10121213 http://dx.doi.org/10.1109/cicc57935.2023.10121213

Yip M , Chandrakasan A P . A resolution-reconfigurable 5-to-10-bit 0.4-to-1 V power scalable SAR ADC for sensor applications [J ] . IEEE Journal of Solid-State Circuits , 2013 , 48 ( 6 ): 1453 - 1464 . DOI: 10.1109/jssc.2013.2254551 http://dx.doi.org/10.1109/jssc.2013.2254551

郭仲杰 , 苏昌勖 , 许睿明 , 等 . 基于粗细量化并行与TDC混合的CMOS图像传感器列级ADC设计方法 [J ] . 电子学报 , 2024 , 52 ( 2 ): 486 - 499 . DOI: 10.12263/DZXB.20220744 http://dx.doi.org/10.12263/DZXB.20220744

Guo Zhongjie , Su Changxu , Xu Ruiming , et al . Column level ADC design method of CMOS image sensor based on coarse and fine quantization parallel and TDC hybrid [J ] . Acta Electronica Sinica , 2024 , 52 ( 2 ): 486 - 499 . (in Chinese) . DOI: 10.12263/DZXB.20220744 http://dx.doi.org/10.12263/DZXB.20220744

Dikopoulos E , Hsu Y T , Wormald L , et al . 25.1 a physics-inspired oscillator-based mixed-signal optimization engine for solving 50-variable 218-clause 3-SAT problems with 100% solvability and 31.7 μs solution time [C ] // 2025 IEEE International Solid-State Circuits Conference . San Francisco : IEEE , 2025 : 10904814 . DOI: 10.1109/isscc49661.2025.10904814 http://dx.doi.org/10.1109/isscc49661.2025.10904814

Wu Zihan , Tang Xiyuan , Zhang Tao , et al . SKADI: A 28-nm complete K-SAT solver featuring bidirectional in-memory deduction and incremental updating [J ] . IEEE Journal of Solid-State Circuits , 2026 , 61 ( 5 ): 1 - 14 . DOI: 10.1109/jssc.2025.3598289 http://dx.doi.org/10.1109/jssc.2025.3598289

Yan Bonan , Liu Mengyun , Chen Yiran , et al . On designing efficient and reliable nonvolatile memory-based computing-in-memory accelerators [C ] // 2019 IEEE International Electron Devices Meeting . San Francisco : IEEE , 2020 : 8993562 . DOI: 10.1109/iedm19573.2019.8993562 http://dx.doi.org/10.1109/iedm19573.2019.8993562

浏览量

106

下载量

CSCD

文章被引用时，请邮件提醒。

提交

工具集

关联资源

基于层间特征图压缩的卷积神经网络加速器

RTL级可扩展高性能数据压缩方法实现

动态二部图上高效的BiCore-索引维护算法

面向近海的多基站协作通信感知一体化设计

知识增强的区域关联图像解说生成方法