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

更新时间：2026-03-26

- Multilevel Resistive Memory Enabled Parallel-gradient Boolean Satisfiability Solver with Clause-folding Scheme
- ACTA ELECTRONICA SINICA Pages: 1-12(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，
  
  Online First：26 March 2026，
- 稿件说明：
移动端阅览
YUE Wenshuo, YE Lintao, SHI Daijing, et al. Multilevel Resistive Memory Enabled Parallel-gradient Boolean Satisfiability Solver with Clause-folding Scheme[J/OL]. ACTA ELECTRONICA SINICA, 2026, 1-12.
DOI：

YUE Wenshuo, YE Lintao, SHI Daijing, et al. Multilevel Resistive Memory Enabled Parallel-gradient Boolean Satisfiability Solver with Clause-folding Scheme[J/OL]. ACTA ELECTRONICA SINICA, 2026, 1-12. 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 .

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 .

Marques-Silva J . Practical applications of Boolean satisfiability [C ] // 2008 9th international workshop on discrete event systems . Gothenburg : IEEE , 2008 : 74 - 80 .

Ganai M K , Gupta A . SAT-based scalable formal verification solutions [M ] . New York : Springer , 2007 .

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 .

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 .

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 : 1 - 6 .

Martins R , Manquinho V , Lynce I . An overview of parallel SAT solving [J ] . Constraints , 2012 , 17 ( 3 ): 304 - 347 .

Goldberg E , Novikov Y . BerkMin: A fast and robust sat-solver [J ] . Discrete Applied Mathematics , 2007 , 155 ( 12 ): 1549 - 1561 .

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 .

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 .

Kim D , Rahman N M , Mukhopadhyay S . 29.1 a 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 .

Bhattacharya T , Hutchinson G H , Pedretti G , et al . Computing high-degree polynomial gradients in memory [J ] . Nature Communications , 2024 , 15 ( 1 ): 8211 .

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 .

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 .

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 .

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 .

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 .

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 .

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 .

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

Li Jianing , Yao Peng , Lu Jie , et al . Research status of computing-in-memory technology [J ] . Acta Electronica Sinica , 2024 , 52 ( 4 ): 1103 - 1117 . (in Chinese)

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 .

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 .

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 .

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 ): 2302658 .

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 .

Rao Mingyi , Tang Hao , Wu Jiangbin , et al . Thousands of conductance levels in memristors integrated on CMOS [J ] . Nature , 2023 , 615 ( 7954 ): 823 - 829 .

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 : 1 - 2 .

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 .

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

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)

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 : 1 - 3 .

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 , 2025 : 1 - 14 .

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 : 14.5.1- 14 . 5 . 4 .

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Implementation of RTL Scalable High-Performance Data Compression Method

Research on Multi-Dimensional Data Compression Algorithm for Cluster-Based Routing in Wireless Sensor Network

A New Test Data Compression and Decompression Technique Based on Statistic Relativity of Variable Length Data Block

A Compression Method with Wavelet Transformation and Biblock Zero Tree Coding

Related Author

CHEN Xiao-jie

LI Bin

ZHOU Qing-lei

OUYANG Dan-tong

ZHAO Xiang-fu

YIN Zhen-yu

ZHAO Hai

XU Jiu-qiang

Related Institution

State Key Laboratory of Mathematical Engineering and Advanced Computing

School of Computer and Artificial Intelligence, Zhengzhou University

Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education Jilin UniversityChangchunJilin130012China

School of Computer Science and TechnologyJilin UniversityChangchunJilin 130012China

Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education, Jilin University

⁰