This paper describes SatIn, a hardware accelerator for determining boolean satisfiability (SAT) -- an important problem in many domains including verification, security analysis, and planning. SatIn is based on a distributed associative array which performs short, atomic operations that can be composed into high level operations. To overcome scaling limitations imposed by wire delay, we extended the algorithms used in software solvers to function efficiently on a distributed set of nodes communicating with message passing. A cycle-level simulation on real benchmarks shows that SatIn achieves an average 72x speedup against Glucose, the winner of 2016 SAT competition, with the potential to achieve a 113x speedup using two contexts. To quantify SatIn's physical requirements, we placed and routed a single clause using the Synopsys 32nm} educational development kit. We were able to meet a 1ns cycle constraint with our target clause fitting in 4867um^2 and consuming 63.8uW of dynamic power; with a network, this corresponds to 100k clauses consuming 8.3W of dynamic power (not including leakage or global clock power) in a 500mm^2 32nm chip.

翻译：本文介绍了SatIn，一种用于判定布尔可满足性（SAT）的硬件加速器——该问题在验证、安全分析和规划等众多领域中至关重要。SatIn基于分布式关联阵列，执行可组合为高层操作的短原子操作。为克服线延迟带来的扩展限制，我们将软件求解器中使用的算法加以扩展，使其能在通过消息传递进行通信的分布式节点集上高效运行。对真实基准测试的周期级仿真表明，与2016年SAT竞赛冠军Glucose相比，SatIn平均实现了72倍加速，且有望通过利用两个上下文达到113倍加速。为量化SatIn的物理需求，我们使用Synopsys 32纳米教育开发套件对单个子句进行了布局布线。我们得以满足1纳秒周期约束，目标子句占用4867平方微米面积，动态功耗为63.8微瓦；在网络上，这相当于在500平方毫米的32纳米芯片中，10万个子句消耗8.3瓦动态功耗（不包括泄漏或全局时钟功耗）。