A 32.5mW Mixed-Signal Processing-in-Memory-Based k-SAT Solver in 65nm CMOS with 74.0% Solvability for 30-Variable 126-Clause 3-SAT Problems

📋 论文概要

该论文提出了一种基于混合信号处理存内计算（Processing-in-Memory）的k-SAT求解器，在65nm CMOS工艺中实现，功耗仅32.5mW。针对30变量126子句的k-SAT问题，该求解器达到了74.0%的求解率，显著优于此前16%的求解率水平，解决了传统硬件求解器对复杂问题求解率低的问题。

💡 主要创新点

• 首次采用混合信号处理存内计算架构实现k-SAT求解器，将存储与计算融合以降低数据搬移开销。
• 在低功耗（32.5mW）条件下实现了74.0%的高求解率，针对30变量126子句的复杂问题显著超越先前设计。
• 通过模拟计算单元与随机搜索机制结合，提升了NP完全组合优化问题的求解效率。

🏷 关键词

📄 原文摘要

Boolean satisfiability (k-SAT, k ≥3) is an NP-complete combinatorial optimization problem (COP) with applications in communication, flight network, supply chain and finance, to name a few. The ASICs for SAT and other COP solvers have been demonstrated using continuous-time dynamics [1], simulated annealing [2], oscillator interaction [3] and stochastic automata annealing [4]. However, prior designs show low solvability for complex problems ([1] shows 16% solvability for 30 variables and 126 clauses), and use a small, fixed network topology (King’s graph [3] or Lattice Graph [2] or 3-SAT [1]) limiting the flexibility of problem solving. A digital fully connected processor enables flexibility but incurs a large area, latency and power overhead [4]. This paper presents a k-SAT solver where a Continuous-Time Stochastic Recurrent Neural Network (CT-SRNN), controlled by a Discrete-Time Finite-State-Machine (DT-FSM), uses

👥 作者与机构

Daehyun Kim, Nael Mizanur Rahman, Saibal Mukhopadhyay

Georgia Institute of Technology, Atlanta, GA