Multilevel Resistive Memory Enabled Parallel-Gradient Boolean Satisfiability Solver with Clause-Folding Scheme

YUE Wenshuo; YE Lintao; SHI Daijing; FU Yihan; YANG Yuxiang; ZHAO Hongxiao; LI Jiayi; ZHANG Teng; YAN Bonan; YANG Yuchao

doi:10.12263/DZXB.20250966

您当前的位置：

首页 >

文章列表页 >

Multilevel Resistive Memory Enabled Parallel-Gradient Boolean Satisfiability Solver with Clause-Folding Scheme

Innovative Architectures and Electronic Systems for Efficient Artificial Intelligence | 更新时间：2026-10-16

- Multilevel Resistive Memory Enabled Parallel-Gradient Boolean Satisfiability Solver with Clause-Folding Scheme
- ACTA ELECTRONICA SINICA Vol. 54, Issue 6, Pages: 2403-2414(2026)
- 作者机构：
  
  1.北京大学集成电路学院/集成电路高精尖创新中心新基石科学实验室，北京 100871
  2.北京大学人工智能研究院，北京 100871
  3.北京大学信息科学技术学院，北京 100871
  4.北京大学信息工程学院广东省存算一体芯片重点实验室新基石科学实验室，广东深圳 518055
  5.北京脑科学与类脑研究所，北京 102206
- 作者简介：
- 基金信息：
  
  National Key Research and Development Program of China(2023YFB4502200);National Natural Science Foundation of China(92164302;92364102;T2350006);Guangdong Provincial Key Laboratory of In-Memory Computing Chips(2024B1212020002);Beijing Natural Science Foundation(L234026;L257010);111 Project(B18001);This work has been supported by the New Cornerstone Science Foundation
- DOI：10.12263/DZXB.20250966
  CLC： TP302.1;TP389.1
- Received：27 November 2025，
  
  Accepted：22 December 2025，
  
  Published：25 June 2026
- 稿件说明：
移动端阅览
岳文硕, 叶林韬, 史代璟, 等. 基于多值阻变存储器与子句折叠策略的并行梯度布尔可满足性求解器[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

Views

106

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

A Convolutional Neural Network Accelerator Based on Inter-Layer Feature Map Compression

Implementation of RTL Scalable High-Performance Data Compression Method

Joint Optimization Strategy for Real-Time Video Transmission Assisted by Drones in Emergency Scenarios

Knowledge-Augmented Grounded Image Narrative Generation

MDW: The Minimum Double-Weight of Differential Characteristics Searching Model

Related Author

YE Lintao

BU Wenjie

XIE Liangbo

CHEN Lin

ZHOU Mu

ZHOU Qing-lei

LI Bin

CHEN Xiao-jie

Related Institution

School of Electronic Science and Engineering, Chongqing University of Posts and Telecommunications

School of Communications and Information Engineering, Chongqing University of Posts and Telecommunications

State Key Laboratory of Mathematical Engineering and Advanced Computing

School of Computer and Artificial Intelligence, Zhengzhou University

School of Computer Science and Technology, Jilin University

⁰