SKADI: A 28nm Complete K-SAT Solver Featuring Dual-Path SRAM-Based Macro and Incremental Update with 100% Solvability

📋 论文概要

该论文提出了一种基于28nm工艺的完整K-SAT求解器SKADI，采用双路径SRAM宏和增量更新技术，实现了100%的可解性，解决了传统Von Neumann架构求解K-SAT问题能耗高、速度慢的问题。

💡 主要创新点

• 提出双路径SRAM宏结构，支持高效并行搜索，加速求解过程。
• 采用增量更新机制，减少重复计算，提高求解效率。
• 实现100%可解性，确保所有K-SAT实例都能被求解，克服了传统求解器的不完备性。

🏷 关键词

📄 原文摘要

applications in various fields, including electronic design automation [1], formal verification [2], and fault diagnosis [3]. The objective of the K-SAT problem is to determine whether a truth assignment exists for n Boolean variables Xi to satisfy all clauses that typically are in conjunctive normal form F(x). Given its NP-complete nature, solving K-SAT problems on Von Neumann machines consumes extensive energy and time. To address this challenge, several ASIC solvers have been proposed, employing diverse methods such as continuoustime dynamics [4], Ising machines [5], and recurrent neural networks [6]. However, all prior works [4-8] are incomplete solvers that are only capable of resolving satisfiable (SAT) cases, without providing proof for the unsatisfiability (UNSAT) of F(x). This constraint limits

👥 作者与机构

Zihan Wu, Xiyuan Tang, Tao Zhang, Lishan Lin, Haoyang Luo, Bocheng Xu,

Zhongyi Wu, Jiahao Song, Yitao Liang, Xiaochen Bo, Yuan Wang Peking University, Beijing, China Boolean satisfiability (K-SAT, K%3) is an NP-complete problem that has