TY - GEN
T1 - Amoeba-Inspired Stochastic Hardware SAT Solver
AU - Hara, Kazuaki
AU - Takeuchi, Naoki
AU - Aono, Masashi
AU - Hara-Azumi, Yuko
N1 - Funding Information:
ACKNOWLEDGMENT he authors acknowledge support from VLSI Design and Education Center (VDEC), the University of Tokyo, in collaboration with Synopsys, Inc. This work is partially supported by JSPS KAKENHI 17H04677 and PRESTO (No. JPMJPR1528) from the Japan Science and Technology Agency (JST).
Publisher Copyright:
© 2019 IEEE.
PY - 2019/4/23
Y1 - 2019/4/23
N2 - Since the end of Dennard scaling is almost approaching, new types of computing methods and architectures are being sought. As one of such architectures, hardware solvers for 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, fast FPGA-based SAT solver with fine-grained parallelism. We particularly focus on a recently-developed SAT algorithm, AmoebaSAT, which abstracts shape-changing dynamics of an amoeba. Our hardware AmoebaSAT solver can enjoy high parallelism in quickly 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 on WalkSAT, another SAT algorithm which has been popular and widely-used for decades.
AB - Since the end of Dennard scaling is almost approaching, new types of computing methods and architectures are being sought. As one of such architectures, hardware solvers for 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, fast FPGA-based SAT solver with fine-grained parallelism. We particularly focus on a recently-developed SAT algorithm, AmoebaSAT, which abstracts shape-changing dynamics of an amoeba. Our hardware AmoebaSAT solver can enjoy high parallelism in quickly 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 on WalkSAT, another SAT algorithm which has been popular and widely-used for decades.
UR - http://www.scopus.com/inward/record.url?scp=85065207408&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85065207408&partnerID=8YFLogxK
U2 - 10.1109/ISQED.2019.8697729
DO - 10.1109/ISQED.2019.8697729
M3 - Conference contribution
AN - SCOPUS:85065207408
T3 - Proceedings - International Symposium on Quality Electronic Design, ISQED
SP - 151
EP - 156
BT - Proceedings of the 20th International Symposium on Quality Electronic Design, ISQED 2019
PB - IEEE Computer Society
T2 - 20th International Symposium on Quality Electronic Design, ISQED 2019
Y2 - 6 March 2019 through 7 March 2019
ER -