Solving satisfiability problems using reconfigurable computing

Takayuki Suyama, Makoto Yokoo, Hiroshi Sawada, Akira Nagoya

Research output: Contribution to journalArticle

32 Citations (Scopus)

Abstract

This paper reports on an innovative approach for solving satisfiability problems for propositional formulas in conjunctive normal form (SAT) by creating a logic circuit that is specialized to solve each problem instance on field programmable gate arrays (FPGAs). This approach has become feasible due to recent advances in reconfigurable computing and has opened up an exciting new research field in algorithm design. SAT is an important subclass of constraint satisfaction problems, which can formalize a wide range of application problems. We have developed a series of algorithms that are suitable for logic circuit implementation, including an algorithm whose performance is equivalent to the Davis-Putnam procedure with powerful dynamic variable ordering. Simulation results show that this method can solve a hard random 3-SAT problem with 400 variables within 1.6 min at a clock rate of 10 MHz. Faster speeds can be obtained by increasing the clock rate. Furthermore, we have actually implemented a 128-variable 256-clause problem instance on FPGAs.

Original languageEnglish
Pages (from-to)109-116
Number of pages8
JournalIEEE Transactions on Very Large Scale Integration (VLSI) Systems
Volume9
Issue number1
DOIs
Publication statusPublished - Feb 1 2001

Fingerprint

Logic circuits
Field programmable gate arrays (FPGA)
Clocks
Constraint satisfaction problems

All Science Journal Classification (ASJC) codes

  • Software
  • Hardware and Architecture
  • Electrical and Electronic Engineering

Cite this

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

In: IEEE Transactions on Very Large Scale Integration (VLSI) Systems, Vol. 9, No. 1, 01.02.2001, p. 109-116.

Research output: Contribution to journalArticle

Suyama, Takayuki ; Yokoo, Makoto ; Sawada, Hiroshi ; Nagoya, Akira. / Solving satisfiability problems using reconfigurable computing. In: IEEE Transactions on Very Large Scale Integration (VLSI) Systems. 2001 ; Vol. 9, No. 1. pp. 109-116.
@article{6af7e52900be4670b96400e23da8fdf7,
title = "Solving satisfiability problems using reconfigurable computing",
abstract = "This paper reports on an innovative approach for solving satisfiability problems for propositional formulas in conjunctive normal form (SAT) by creating a logic circuit that is specialized to solve each problem instance on field programmable gate arrays (FPGAs). This approach has become feasible due to recent advances in reconfigurable computing and has opened up an exciting new research field in algorithm design. SAT is an important subclass of constraint satisfaction problems, which can formalize a wide range of application problems. We have developed a series of algorithms that are suitable for logic circuit implementation, including an algorithm whose performance is equivalent to the Davis-Putnam procedure with powerful dynamic variable ordering. Simulation results show that this method can solve a hard random 3-SAT problem with 400 variables within 1.6 min at a clock rate of 10 MHz. Faster speeds can be obtained by increasing the clock rate. Furthermore, we have actually implemented a 128-variable 256-clause problem instance on FPGAs.",
author = "Takayuki Suyama and Makoto Yokoo and Hiroshi Sawada and Akira Nagoya",
year = "2001",
month = "2",
day = "1",
doi = "10.1109/92.920826",
language = "English",
volume = "9",
pages = "109--116",
journal = "IEEE Transactions on Very Large Scale Integration (VLSI) Systems",
issn = "1063-8210",
publisher = "Institute of Electrical and Electronics Engineers Inc.",
number = "1",

}

TY - JOUR

T1 - Solving satisfiability problems using reconfigurable computing

AU - Suyama, Takayuki

AU - Yokoo, Makoto

AU - Sawada, Hiroshi

AU - Nagoya, Akira

PY - 2001/2/1

Y1 - 2001/2/1

N2 - This paper reports on an innovative approach for solving satisfiability problems for propositional formulas in conjunctive normal form (SAT) by creating a logic circuit that is specialized to solve each problem instance on field programmable gate arrays (FPGAs). This approach has become feasible due to recent advances in reconfigurable computing and has opened up an exciting new research field in algorithm design. SAT is an important subclass of constraint satisfaction problems, which can formalize a wide range of application problems. We have developed a series of algorithms that are suitable for logic circuit implementation, including an algorithm whose performance is equivalent to the Davis-Putnam procedure with powerful dynamic variable ordering. Simulation results show that this method can solve a hard random 3-SAT problem with 400 variables within 1.6 min at a clock rate of 10 MHz. Faster speeds can be obtained by increasing the clock rate. Furthermore, we have actually implemented a 128-variable 256-clause problem instance on FPGAs.

AB - This paper reports on an innovative approach for solving satisfiability problems for propositional formulas in conjunctive normal form (SAT) by creating a logic circuit that is specialized to solve each problem instance on field programmable gate arrays (FPGAs). This approach has become feasible due to recent advances in reconfigurable computing and has opened up an exciting new research field in algorithm design. SAT is an important subclass of constraint satisfaction problems, which can formalize a wide range of application problems. We have developed a series of algorithms that are suitable for logic circuit implementation, including an algorithm whose performance is equivalent to the Davis-Putnam procedure with powerful dynamic variable ordering. Simulation results show that this method can solve a hard random 3-SAT problem with 400 variables within 1.6 min at a clock rate of 10 MHz. Faster speeds can be obtained by increasing the clock rate. Furthermore, we have actually implemented a 128-variable 256-clause problem instance on FPGAs.

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

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

U2 - 10.1109/92.920826

DO - 10.1109/92.920826

M3 - Article

AN - SCOPUS:0035242975

VL - 9

SP - 109

EP - 116

JO - IEEE Transactions on Very Large Scale Integration (VLSI) Systems

JF - IEEE Transactions on Very Large Scale Integration (VLSI) Systems

SN - 1063-8210

IS - 1

ER -