Accelerating Boolean Constraint Propagation for Efficient SAT-Solving on FPGAs

TL;DR

The paper tackles the bottleneck of Boolean Constraint Propagation in DPLL-based SAT solving by building a hardware-accelerated solver on FPGA-SoCs. It eliminates clause lookups by placing each clause directly into a Clause Processor and supports large formulas through runtime partitioning and hot-swapping from external memory, coordinated with a general-purpose processor. The authors present an open-source prototype on a Xilinx Zynq that demonstrates up to 6x overall speedup over software, with additional 1.7x and 1.1x improvements on two benchmarks for BCP. This approach yields significant practical impact for embedded and resource-constrained settings where SAT-solving performance is critical, and it lays groundwork for further optimization via partitioning strategies.

Abstract

We present a hardware-accelerated SAT solver targeting processor/Field Programmable Gate Arrays (FPGA) SoCs. Our solution accelerates the most expensive subroutine of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, Boolean Constraint Propagation (BCP) through fine-grained FPGA parallelism. Unlike prior state-of-the-art solutions, our solver eliminates costly clause look-up operations by assigning clauses directly to clause processors on the FPGA and dividing large formulas into smaller partitions manageable by FPGA. Partitions are hot-swapped during runtime as required and the supported formula size is limited only by available external memory, not on-chip FPGA memory. We evaluate our solver on a Xilinx Zynq platform with results showing quicker execution time across various formula sizes, subject to formula partitioning strategy. Compared to prior state-of-the-art, we achieve 1.7x and 1.1x speed up on BCP for 2 representative benchmarks and up to 6x total speedup over software-only implementation.

Figures (6)

• Figure 1: Interface between processor and FPGA-based BCP Coprocessor. DPLL's BCP is accelerated through fine-grained parallelization across Clause Processors.
• Figure 2: (a) Davis et al. store the formula directly on FPGA. Clauses within partitions contain no shared variables, and partitions are mapped directly to Implication Engines. (b) Thong et al. store formula directly on FPGA. Clauses are linked to other clauses with shared variables and are processed sequentially. (c) Formula stored in external memory ("software" view). Clauses in partitions mapped directly to Clause Processors, and hot-swapped as required.
• Figure 3: Execution steps of each described approach.
• Figure 4: Breakdown of the total execution time across constituent components.
• Figure 5: Effect of increasing clauses size on total execution time, for 63 variables.