⚡ 本页包含 AI 生成的分析内容，仅供参考
本文提出了一款基于28nm CMOS工艺的模式可重构CAM-CIM混合架构的完整3-SAT求解器，支持冲突驱动子句学习（CDCL），解决了传统ASIC求解器交叉映射效率低、忽视社区结构且缺乏适应性等问题。相比最先进的ASIC完整求解器，实现了4.3至5.1倍的加速和1.4倍的能耗降低。
Abstract The K-SAT problem is NP-complete and costly on von Neumann machines. Several ASIC solvers have been proposed to mitigate this, but they rely on inefficient crossbar mapping, overlook community structures and lack adaptability to formula size. This work presents an ASIC complete solver with conflict-driven clause learning (CDCL), employing a modereconfigurable CAM–CIM hybrid architecture. Fabricated in 28nm CMOS, it achieves 4.3-to-5.1× speedup and 1.4× energy reduction over a state-of-the-art ASIC complete solver. The Boolean satisfiability (K-SAT) problem is a fundamental combinatorial problem. Its objective is to find a satisfying (SAT) assignment for a Boolean formula F(x) in conjunctive normal form (CNF), or prove it is unsatisfiable (UNSAT). K-SAT finds applications in many areas, such as formal verification [1], synthesis [2], and AI planning [3]. According to complexity theory [4], K-SAT is NP-complete for all K)3 and can be reduced to 3-SAT with
Zihan Wu, Xiyuan Tang, Lishan Lin, Youming Yang, Haoyang Luo, Bocheng Xu, Yitao Liang, Xiaochen Bo, Yuan Wang
Peking University, Beijing, China