Solving satisfiability problems by using reconfigurable hardware

Takayuki Suyama, Makoto Yokoo, Hiroshi Sawada, Akira Nagoya

Research output: Contribution to journalArticle

Abstract

In this paper, we will propose a new solution method for SAT (Satisfiability Problems) using FPGA (Field-Programmable Gate Arrays) and logic synthesis system. This method is distinctive in that a logic circuit specialized to solve each problem instance is configured on FPGA. This approach has become possible due to the progress in reconfigurable computing technology in recent years and opens a new possibility in design principle of algorithms: SAT is a kind of constraint satisfaction problem and is a general framework which can represent many application problems. In this paper, we will propose various algorithms which are suitable for implementation on hardware. Among these algorithms, the one which has the highest performance has a performance equal to the Davis-Putman algorithm which introduced the heuristic with dynamic ordering of variables. From the evaluation results using simulation, we show that by the method proposed herein, the solution of a 3-SAT problem instance with 400 variables generated in a very hard random can be obtained in 1.6 minutes when the circuit is operated at a machine cycle of 10 MHz. Moreover, a very hard problem instance with 128 variables and 256 clauses was packaged on FPGAs and its operation was confirmed.

Original languageEnglish
Pages (from-to)35-46
Number of pages12
JournalElectronics and Communications in Japan, Part II: Electronics (English translation of Denshi Tsushin Gakkai Ronbunshi)
Volume86
Issue number3
DOIs
Publication statusPublished - Mar 1 2003
Externally publishedYes

Keywords

  • Constraint satisfaction problem
  • FPGA
  • Logic synthesis
  • Reconfigurable computing
  • Satisfiability problem

ASJC Scopus subject areas

  • Physics and Astronomy(all)
  • Computer Networks and Communications
  • Electrical and Electronic Engineering

Fingerprint Dive into the research topics of 'Solving satisfiability problems by using reconfigurable hardware'. Together they form a unique fingerprint.

  • Cite this