Efficient FPGA Implementation of Amoeba-inspired SAT Solver with Feedback and Bounceback Control: Harnessing Variable-Level Parallelism for Large-Scale Problem Solving in Edge Computing

The Boolean satisfiability problem (SAT), an NP-complete problem, poses significant challenges for conventional general-purpose computers due to its inherent “combinatorial explosion” nature. Fast SAT solvers, however, offer immense potential for smart city applications, such as optimal planning and scheduling in logistics and communication, driving the need for innovative solving methods. Implementing a high-speed SAT solver on a field programmable gate array (FPGA) by exploiting its variable-level parallelism and energy efficiency is a promising approach for applications requiring time-critical control and low energy consumption at the network edge. Inspired by the deformation behavior of an amoeboid organism, the "AmoebaSAT" algorithm has emerged as a novel solution search process for the SAT problem, enabling the parallel updating of all state variables. Although state-of-the-art studies on FPGA-implemented AmoebaSATs have successfully addressed smaller 3-SAT instances with several hundred variables, they adopt an instance-specific approach, requiring pre-processing or synthesizing the FPGA configuration each time the targeted SAT instance changes. This study introduces a modified algorithm, “AmoebaSATone,” incorporating a novel feedback control mechanism alongside the original bounceback control for more efficient resource utilization. The authors implement AmoebaSATone on a Zynq FPGA board, employing an instance-general approach that targets arbitrary instances without regenerating configuration data, while facilitating easy algorithm setting updates. FPGA-implemented AmoebaSATone effectively solves large 3-SAT instances with problem sizes up to 120,000 variables (523,200 clauses), previously unattainable on a single FPGA board. Compared to a CPU implementation on a Ryzen server, the FPGA-AmoebaSATone achieved a speedup ranging from 3.2 to 14.8 times. These results showcase the potential of the AmoebaSATone algorithm for solving SAT-based problems on a larger scale, paving the way for further research on dedicated edge-oriented problem-solving hardware.