SharpSAT: A Heuristic-Learning-Based SAT Accelerator Achieving 0.8μs/16.1μs Solution Time in SAT/UNSAT Cases

📋 论文概要

本文提出SharpSAT，一种基于启发式学习的布尔可满足性（SAT）问题加速器，在28nm工艺上实现了SAT/UNSAT情况下0.8μs/16.1μs的快速求解时间。通过快速子句学习单元、双BCP单元和启发式变量决策器，相比先前加速器获得21.11倍/2.61倍的加速比。

💡 主要创新点

• 设计了快速子句学习单元，通过从冲突中推导约束来剪枝搜索空间。
• 提出双BCP（布尔约束传播）单元，加速蕴涵传播过程。
• 引入启发式变量决策器，利用非确定性高效遍历解空间。

🏷 关键词

📄 原文摘要

Abstract We present SharpSAT, a heuristic-learning SAT accelerator that achieves fast solution times of 0.8$s for SAT and 16.1$s for UNSAT cases. Our design integrates: a fast clause learning unit that prunes the search space by deriving constraints from conflicts; a dual-BCP unit that accelerates implication propagation; and a heuristic variable decider introducing nondeterminism to efficiently traverse the solution space. A 28nm prototype demonstrates 21.11×/2.61× (SAT/UNSAT) speedup over prior accelerators. The Boolean satisfiability (SAT) problem, a proven NP-complete problem, sits at the core of modern computational tasks, from circuit verification and cryptographic analysis to AI planning [1]. A SAT instance asks for a set of Boolean assignments that make all clauses in a conjunctive normal form (CNF) evaluate to TRUE. Conventionally, solving the SAT problem using software can be time-consuming, and several ASIC accelerators have been

👥 作者与机构

Yi Huang, Hao Kong, Iris Ying Chou, Bin Wang, Xiangyu Kong, Jianfeng Zhu, Liangwei Li, Xiao Li, Hanning Wang, Aoyang Zhang, Leibo Liu

Tsinghua University, Beijing, China