FPGA acceleration of enhanced boolean constraint propagation for SAT solvers
FPGA acceleration of enhanced boolean constraint propagation for SAT solvers
复制标题
SAT 求解器的增强型布尔约束传播的 FPGA 加速
DOI：
--
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
N. Nicolici
中科院分区：
文献类型：
--
作者：
J. Thong;N. Nicolici
我们提出了一个硬件体系结构来加速布尔约束传播（BCP）。尽管软件中的满意度（SAT）求解器使用不同的搜索和学习策略，但BCP是一个基本组成部分，到目前为止，CPU时间最多。我们的现场编程门阵列（FPGA）设计使用片上SRAM来促进BCP的加速度。我们讨论了我们创新的硬件内存布局的许多见解，这非常紧凑，可以实现非常快的BCP。它还支持多线程，以最大程度地减少硬件中的空闲时间并充分利用多核心处理器主机。此外，许多工业SAT实例将逻辑门编码为约束。我们将这些压缩以同时减少硬件存储器的使用情况以及加快计算（增强的BCP）。我们实施了增强的BCP核心，并将其与一个简单的软件SAT求解器集成在一起，该软件通过PCI Express进行了通信。硬件性能计数器表明，单个处理引擎比最先进的软件SAT求解器快4倍。
We propose a hardware architecture to accelerate boolean constraint propagation (BCP). Although satisfiability (SAT) solvers in software use varying search and learning strategies, BCP is a fundamental component and by far consumes the most CPU time. Our field-programmable gate array (FPGA) design uses on-chip SRAM to facilitate the acceleration of BCP. We discuss many insights to our innovative hardware memory layout, which is very compact and enables extremely fast BCP. It also supports multithreading to minimize the idle time in hardware and to fully utilize the multicore processor host. Additionally, many industrial SAT instances encode logic gates as constraints. We compact these to simultaneously reduce the hardware memory usage as well as speed up the computation (enhanced BCP). We implemented our enhanced BCP core and integrated it with a simple software SAT solver which communicates over PCI Express. Hardware performance counters show that a single processing engine is up to 4x faster than a state-of-the-art software SAT solver.