An effective probability distribution SAT solver on reconfigurable hardware

摘要

Boolean Satisfiability (SAT) is an important problem both theoretically and for a variety of practical applications. While the general SAT problem is NP complete, advanced solver algorithms and heuristics can provide fast and efficient solving of otherwise intractable problems. While much advancement has been made with Conflict Driven Clause Learning (CDCL) based sequential solvers, Stochastic Local Search (SLS) solvers such as WalkSAT, Sparrow and probSAT have proven effective for certain instance types. SLS solvers are well suited to parallelization and hardware implementation due to the simplified control flow and lack of data dependencies between solver instances started with different seeds. This paper presents a hardware implementation of the probSAT algorithm using High-Level Synthesis (HLS) for rapid porting of the design from the original C implementation. Specifically, the presented approach shows very strong performance on the class of small, but difficult SAT problems with speedups between 89-828x over MiniSAT and 5-99x over the software implementation of probSAT on such problems.