FPGA-Based Hardware/Software Co-Design of a Bio-Inspired SAT Solver

Abstract

For various kinds of Internet of Things (IoT) systems whose control rules can be expressed in a Satisfiability (SAT) problem, this work aims at realizing an IoT-oriented FPGA-based SAT solver leveraging a bio-inspired algorithm, AmoebaSAT, using a hardware/software co-design approach. With regard to the software component, we extended the baseline algorithm to escape from local minima more quickly and achieve significant reduction in iteration count. With regard to hardware, we fully extracted the fine-grained parallelism of the algorithm to further accelerate the solution search. Through our evaluations using several benchmarks of varying variable count and complexity, we demonstrated the efficiency of our solver, especially for larger practical SAT instances. Compared with three state-of-the-art solvers (i.e., one software implementation of the original AmoebaSAT algorithm and two FPGA-based hardware solvers), we achieved an average of $15.9\times $ and up to $48\times $ reduction in iteration count. Furthermore, through in-depth analyses of the experimental results, we provided the essential findings on the relationship between the problem's complexity and the SAT algorithm that can be leveraged for extensions of both the hardware and software designs.