Snap-SAT: A One-Shot Energy-Performance-Aware All-Digital Compute-in-Memory Solver for Large-Scale Hard Boolean Satisfiability Problems

📋 论文概要

本文提出Snap-SAT，一种基于全数字存内计算（CIM）的一次性求解器，用于加速大规模硬布尔可满足性（SAT）问题。该求解器通过能量性能感知设计，在单次操作中完成求解，显著降低延迟和能耗。

💡 主要创新点

• 首次提出全数字存内计算架构用于SAT求解，实现一次性（one-shot）求解，无需迭代搜索。
• 引入能量性能感知优化机制，平衡求解速度与功耗，适用于大规模硬SAT实例。
• 全数字电路设计，兼容先进CMOS工艺，易于扩展和集成。

🏷 关键词

📄 原文摘要

Sirish Oruganti, Jaydeep P. Kulkarni University of Texas, Austin, TX Boolean satisfiability (SAT) is a non-deterministic polynomial time (NP)-complete problem with many practical and industrial data-intensive applications [1]. Examples (Fig. 29.2.1) include anti-aircraft mission planning in defense, gene prediction in vaccine development, network routing in the data center, automatic test pattern generation in electronic design automation (EDA), and model checking in software. The objective of a SAT solver is to identify the values of n Boolean variables xi that satisfy all clauses in a conjunctive normal form (CNF) [5]. However, the time required to determine the satisfiability of a SAT problem increases exponentially with respect to the variable size, which is energy and resource-consuming. A prior software SAT solver [3] requires frequent data transfer and memory access due to the CPU computations, solution-search,

👥 作者与机构

Shanshan Xie, Mengtian Yang, S. Andrew Lanham, Yipeng Wang, Meizhi Wang,