FPGA-Based Stochastic Local Search Satisfiability Solvers Exploiting High Bandwidth Memory

Boolean Satisfiability (SAT) problems for realistic applications are becoming increasingly large and complex, making it difficult for deterministic methods to be used on modern CPUs. In this paper we present hardware Stochastic Local Search (SLS) solvers that utilize a state-of-the-art FPGA-based accelerator. The method uses well-known SLS heuristics implemented on an accelerator with large memory capacity using the Vitis HLS system. The solver can be reconfigured with multiple SLS kernels to take advantage of the resources on the Alveo U280 accelerator. Combined, our techniques achieve faster convergence on large SAT problems compared to CPU solvers.