Resource-saving FPGA Implementation of the Satisfiability Problem Solver: AmoebaSATslim

Ying Jie Yan, Hideharu Amano, Masashi Aono, Kaori Ohkoda, Shingo Fukuda, Kenta Saito, Seiya Kasai

研究成果: Conference contribution

1 被引用数 (Scopus)

抄録

The Boolean satisfiability problem (SAT) is an NP-complete combinatorial optimization problem, where fast SAT solvers are useful for various smart society applications. Since these edge-oriented applications require time-critical control, a high speed SAT solver on FPGA is a promising approach. Here the authors propose a novel FPGA implementation of a bio-inspired stochastic local search algorithm called 'AmoebaSAT' on a Zynq board. Previous studies on FPGA-AmoebaSATs tackled relatively smaller-sized 3-SAT instances with a few hundred variables and found the solutions in several milli seconds. These implementations, however, adopted an instance-specific approach, which requires synthesis of FPGA configuration every time when the targeted instance is altered. In this paper, a slimmed version of AmoebaSAT named 'AmoebaSATslim,' which omits the most resource-consuming part of interactions among variables, is proposed. The FPGA-AmoebaSATslim enables to tackle significantly larger-sized 3-SAT instances, accepting 30,000 variables with 130, 800 clauses. It achieves up to approximately 24 times faster execution speed than the software-AmoebaSATslim implemented on a CPU of the x86 server.

本文言語English
ホスト出版物のタイトル2021 International Conference on Field-Programmable Technology, ICFPT 2021
出版社Institute of Electrical and Electronics Engineers Inc.
ISBN(電子版)9781665420105
DOI
出版ステータスPublished - 2021
イベント20th International Conference on Field-Programmable Technology, ICFPT 2021 - Virtual, Auckland, New Zealand
継続期間: 2021 12月 62021 12月 10

出版物シリーズ

名前2021 International Conference on Field-Programmable Technology, ICFPT 2021

Conference

Conference20th International Conference on Field-Programmable Technology, ICFPT 2021
国/地域New Zealand
CityVirtual, Auckland
Period21/12/621/12/10

ASJC Scopus subject areas

  • コンピュータ サイエンスの応用
  • コンピュータ ビジョンおよびパターン認識
  • ソフトウェア

フィンガープリント

「Resource-saving FPGA Implementation of the Satisfiability Problem Solver: AmoebaSATslim」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。

引用スタイル