Amoeba-Inspired Stochastic Hardware SAT Solver

Kazuaki Hara, Naoki Takeuchi, Masashi Aono, Yuko Hara-Azumi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the 20th International Symposium on Quality Electronic Design, ISQED 2019
PublisherIEEE Computer Society
Pages151-156
Number of pages6
ISBN (Electronic)9781728103921
DOIs
Publication statusPublished - 2019 Apr 23
Event20th International Symposium on Quality Electronic Design, ISQED 2019 - Santa Clara, United States
Duration: 2019 Mar 62019 Mar 7

Publication series

NameProceedings - International Symposium on Quality Electronic Design, ISQED
Volume2019-March
ISSN (Print)1948-3287
ISSN (Electronic)1948-3295

Conference

Conference20th International Symposium on Quality Electronic Design, ISQED 2019
CountryUnited States
CitySanta Clara
Period19/3/619/3/7

Fingerprint

Hardware
Combinatorial optimization
Embedded systems
Field programmable gate arrays (FPGA)
Internet of things

ASJC Scopus subject areas

  • Hardware and Architecture
  • Electrical and Electronic Engineering
  • Safety, Risk, Reliability and Quality

Cite this

Hara, K., Takeuchi, N., Aono, M., & Hara-Azumi, Y. (2019). Amoeba-Inspired Stochastic Hardware SAT Solver. In Proceedings of the 20th International Symposium on Quality Electronic Design, ISQED 2019 (pp. 151-156). [8697729] (Proceedings - International Symposium on Quality Electronic Design, ISQED; Vol. 2019-March). IEEE Computer Society. https://doi.org/10.1109/ISQED.2019.8697729

Amoeba-Inspired Stochastic Hardware SAT Solver. / Hara, Kazuaki; Takeuchi, Naoki; Aono, Masashi; Hara-Azumi, Yuko.

Proceedings of the 20th International Symposium on Quality Electronic Design, ISQED 2019. IEEE Computer Society, 2019. p. 151-156 8697729 (Proceedings - International Symposium on Quality Electronic Design, ISQED; Vol. 2019-March).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Hara, K, Takeuchi, N, Aono, M & Hara-Azumi, Y 2019, Amoeba-Inspired Stochastic Hardware SAT Solver. in Proceedings of the 20th International Symposium on Quality Electronic Design, ISQED 2019., 8697729, Proceedings - International Symposium on Quality Electronic Design, ISQED, vol. 2019-March, IEEE Computer Society, pp. 151-156, 20th International Symposium on Quality Electronic Design, ISQED 2019, Santa Clara, United States, 19/3/6. https://doi.org/10.1109/ISQED.2019.8697729
Hara K, Takeuchi N, Aono M, Hara-Azumi Y. Amoeba-Inspired Stochastic Hardware SAT Solver. In Proceedings of the 20th International Symposium on Quality Electronic Design, ISQED 2019. IEEE Computer Society. 2019. p. 151-156. 8697729. (Proceedings - International Symposium on Quality Electronic Design, ISQED). https://doi.org/10.1109/ISQED.2019.8697729
Hara, Kazuaki ; Takeuchi, Naoki ; Aono, Masashi ; Hara-Azumi, Yuko. / Amoeba-Inspired Stochastic Hardware SAT Solver. Proceedings of the 20th International Symposium on Quality Electronic Design, ISQED 2019. IEEE Computer Society, 2019. pp. 151-156 (Proceedings - International Symposium on Quality Electronic Design, ISQED).
@inproceedings{e7673eaf05d84d3c810e3493d2c8ee11,
title = "Amoeba-Inspired Stochastic Hardware SAT Solver",
abstract = "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.",
author = "Kazuaki Hara and Naoki Takeuchi and Masashi Aono and Yuko Hara-Azumi",
year = "2019",
month = "4",
day = "23",
doi = "10.1109/ISQED.2019.8697729",
language = "English",
series = "Proceedings - International Symposium on Quality Electronic Design, ISQED",
publisher = "IEEE Computer Society",
pages = "151--156",
booktitle = "Proceedings of the 20th International Symposium on Quality Electronic Design, ISQED 2019",

}

TY - GEN

T1 - Amoeba-Inspired Stochastic Hardware SAT Solver

AU - Hara, Kazuaki

AU - Takeuchi, Naoki

AU - Aono, Masashi

AU - Hara-Azumi, Yuko

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

ER -