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

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

Abstract

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.

Original languageEnglish
Title of host publication2021 International Conference on Field-Programmable Technology, ICFPT 2021
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781665420105
DOIs
Publication statusPublished - 2021
Externally publishedYes
Event20th International Conference on Field-Programmable Technology, ICFPT 2021 - Virtual, Auckland, New Zealand
Duration: 2021 Dec 62021 Dec 10

Publication series

Name2021 International Conference on Field-Programmable Technology, ICFPT 2021

Conference

Conference20th International Conference on Field-Programmable Technology, ICFPT 2021
Country/TerritoryNew Zealand
CityVirtual, Auckland
Period21/12/621/12/10

ASJC Scopus subject areas

  • Computer Science Applications
  • Computer Vision and Pattern Recognition
  • Software

Fingerprint

Dive into the research topics of 'Resource-saving FPGA Implementation of the Satisfiability Problem Solver: AmoebaSATslim'. Together they form a unique fingerprint.

Cite this