SKADI: A 28-nm Complete K-SAT Solver Featuring Bidirectional In-Memory Deduction and Incremental Updating

作者：Zihan Wu, Xiyuan Tang, Tao Zhang, Lishan Lin, Haoyang Luo, Bocheng Xu, Zhongyi Wu, Jiahao Song, Yitao Liang, Xiaochen Bo, Yuan Wang · 发表于：IEEE Journal of Solid-State Circuits · 年份：2025 · DOI：10.1109/jssc.2025.3598289 · 被引用次数：2 · 研究领域：VLSI and FPGA Design Techniques、Advanced Optical Network Technologies、Photonic and Optical Devices

Boolean satisfiability (K-SAT) is a canonical problem at the core of many electronic design automation (EDA) and artificial intelligence (AI) tasks. Due to its NP-complete characteristic, solving K-SAT ($K \geq 3$) problems on von Neumann architectures incurs substantial energy and latency overhead. Recent ASIC K-SAT solvers have significantly improved energy efficiency, but these implementations are inherently incomplete. While these solvers have demonstrated the capability to solve satisfiable (SAT) problems, no evidence has been provided for proving unsatisfiability. This limitation severely restricts their applicability, as real-life scenarios mostly demand definitive SAT/unsatisfiable (UNSAT) outcomes. To address this gap, this work presents a complete K-SAT solver based on the DPLL framework that can determine whether the given formula is SAT or UNSAT. The proposed architecture incorporates a dual-path SRAM-based macro and a position-encoded counter (PEC) to perform highly parallel, bidirectional clause-variable deduction. Additionally, an incremental updating technique is employed for conflict-aware backtracking and search space pruning. Fabricated in 28-nm CMOS, the proposed solver achieves 100% solvability across all SAT and UNSAT benchmarks, with average solution times of$17.1~\mu $s (uf50-218) and$42.1 ~\mu $s (uuf50-218) at 0.9-V supply voltage. Corresponding energy consumptions are 58.0 and 142.8 nJ, respectively. As the first ASIC complete K-SAT solver, it enabl...