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 2003
Externally publishedYes

Fingerprint

reconfigurable hardware
Reconfigurable hardware
problem solving
Field programmable gate arrays (FPGA)
field-programmable gate arrays
Constraint satisfaction problems
logic circuits
Logic circuits
logic
hardware
Hardware
cycles
Networks (circuits)
evaluation
synthesis
simulation

Keywords

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

ASJC Scopus subject areas

  • Electrical and Electronic Engineering

Cite this

Solving satisfiability problems by using reconfigurable hardware. / Suyama, Takayuki; Yokoo, Makoto; Sawada, Hiroshi; Nagoya, Akira.

In: Electronics and Communications in Japan, Part II: Electronics (English translation of Denshi Tsushin Gakkai Ronbunshi), Vol. 86, No. 3, 03.2003, p. 35-46.

Research output: Contribution to journalArticle

@article{5c792414a65b4105aab3a4fa3bca3fab,
title = "Solving satisfiability problems by using reconfigurable hardware",
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.",
keywords = "Constraint satisfaction problem, FPGA, Logic synthesis, Reconfigurable computing, Satisfiability problem",
author = "Takayuki Suyama and Makoto Yokoo and Hiroshi Sawada and Akira Nagoya",
year = "2003",
month = "3",
doi = "10.1002/ecjb.10134",
language = "English",
volume = "86",
pages = "35--46",
journal = "Electronics and Communications in Japan, Part II: Electronics (English translation of Denshi Tsushin Gakkai Ronbunshi)",
issn = "8756-663X",
publisher = "Scripta Technica",
number = "3",

}

TY - JOUR

T1 - Solving satisfiability problems by using reconfigurable hardware

AU - Suyama, Takayuki

AU - Yokoo, Makoto

AU - Sawada, Hiroshi

AU - Nagoya, Akira

PY - 2003/3

Y1 - 2003/3

N2 - 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.

AB - 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.

KW - Constraint satisfaction problem

KW - FPGA

KW - Logic synthesis

KW - Reconfigurable computing

KW - Satisfiability problem

UR - http://www.scopus.com/inward/record.url?scp=0037333735&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0037333735&partnerID=8YFLogxK

U2 - 10.1002/ecjb.10134

DO - 10.1002/ecjb.10134

M3 - Article

AN - SCOPUS:0037333735

VL - 86

SP - 35

EP - 46

JO - Electronics and Communications in Japan, Part II: Electronics (English translation of Denshi Tsushin Gakkai Ronbunshi)

JF - Electronics and Communications in Japan, Part II: Electronics (English translation of Denshi Tsushin Gakkai Ronbunshi)

SN - 8756-663X

IS - 3

ER -