Amoeba-Inspired Stochastic Hardware SAT Solver

Kazuaki Hara1, Naoki Takeuchi2, Masashi Aono3, Yuko Hara-Azumi1
1Tokyo Institute of Technology, 2Yokohama National University, 3Keio University


Since the end of Dennard scaling is almost approaching, new types computing methods and architectures are being sought. As one of such architectures, hardware solvers of satisfiability (SAT) problems are getting more attentions these days because combinatorial optimization problems residing in many types of Internet-of-Things (IoT) and embedded systems applications can be transformed to SAT problems. In this paper, we present a novel, efficient FPGA-based SAT solver with fine-grained parallelism. We particularly focus on a recently-developed SAT algorithm, AmoebaSAT, which was derived from an amoeba's behavior. Our hardware AmoebaSAT solver can enjoy high parallelism in efficiently searching a solution (i.e., a satisfiable combination of variables assignment) for a given SAT instance, with a help of stochastic features to avoid local search. Our evaluations demonstrated that our work can outperform state-of-the-art which is based on WalkSAT, another SAT algorithm which has been popular and widely-used for decades.