Solving satisfiability problems using field programmable gate arrays

First results

Makoto Yokoo, Takayuki Suyama, Hiroshi Sawada

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

12 Citations (Scopus)

Abstract

This paper presents an initial report on an innovative approach for solving satisfiability problems (SAT), i.e., creating a logic circuit that is specialized to solve each problem instance on Field Programmable Gate Arrays (FPGAs). Until quite recently, this approach was unrealistic since creating special-purpose hardware was very expensive and time consuming. However, recent advances in FPGA technologies and automatic logic synthesis technologies have enabled users to rapidly create special-purpose hardware by themselves. This approach brings a new dimension to SAT algorithms, since all constraints (clauses) can be checked simultaneously using a logic circuit. We develop a new algorithm called parallel-checking, which assigns all variable values simultaneously, and checks all constraints concurrently. Simulation results show that the order of the search tree size in this algorithm is approximately the same as that in the Davis-Putnam procedure. Then, we show how the parallel-checking algorithm can be implemented on FPGAs. Currently, actual implementation is under way. We get promising initial results which indicate that we can implement a hard random 3-SAT problem with 300 variables, and run the logic circuit at clock rates of about 1MHz, i.e., it can check one million states per second.

Original languageEnglish
Title of host publicationPrinciples and Practice of Constraint Programming ― CP 1996 - 2nd International Conference, CP 1996, Proceedings
EditorsEugene C. Freuder
PublisherSpringer Verlag
Pages491-509
Number of pages19
ISBN (Print)3540615512, 9783540615514
DOIs
Publication statusPublished - Jan 1 1996
Externally publishedYes
Event2nd International Conference on Principles and Practice of Constraint Programming, CP 1996 - Cambridge, United States
Duration: Aug 19 1996Aug 22 1996

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1118
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other2nd International Conference on Principles and Practice of Constraint Programming, CP 1996
CountryUnited States
CityCambridge
Period8/19/968/22/96

Fingerprint

Logic circuits
Satisfiability Problem
Field Programmable Gate Array
Field programmable gate arrays (FPGA)
Logic
Hardware
Logic Synthesis
Search Trees
Parallel algorithms
Parallel Algorithms
Assign
Clocks
Simulation

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Yokoo, M., Suyama, T., & Sawada, H. (1996). Solving satisfiability problems using field programmable gate arrays: First results. In E. C. Freuder (Ed.), Principles and Practice of Constraint Programming ― CP 1996 - 2nd International Conference, CP 1996, Proceedings (pp. 491-509). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1118). Springer Verlag. https://doi.org/10.1007/3-540-61551-2_96

Solving satisfiability problems using field programmable gate arrays : First results. / Yokoo, Makoto; Suyama, Takayuki; Sawada, Hiroshi.

Principles and Practice of Constraint Programming ― CP 1996 - 2nd International Conference, CP 1996, Proceedings. ed. / Eugene C. Freuder. Springer Verlag, 1996. p. 491-509 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1118).

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

Yokoo, M, Suyama, T & Sawada, H 1996, Solving satisfiability problems using field programmable gate arrays: First results. in EC Freuder (ed.), Principles and Practice of Constraint Programming ― CP 1996 - 2nd International Conference, CP 1996, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1118, Springer Verlag, pp. 491-509, 2nd International Conference on Principles and Practice of Constraint Programming, CP 1996, Cambridge, United States, 8/19/96. https://doi.org/10.1007/3-540-61551-2_96
Yokoo M, Suyama T, Sawada H. Solving satisfiability problems using field programmable gate arrays: First results. In Freuder EC, editor, Principles and Practice of Constraint Programming ― CP 1996 - 2nd International Conference, CP 1996, Proceedings. Springer Verlag. 1996. p. 491-509. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/3-540-61551-2_96
Yokoo, Makoto ; Suyama, Takayuki ; Sawada, Hiroshi. / Solving satisfiability problems using field programmable gate arrays : First results. Principles and Practice of Constraint Programming ― CP 1996 - 2nd International Conference, CP 1996, Proceedings. editor / Eugene C. Freuder. Springer Verlag, 1996. pp. 491-509 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{70d0a451818b47a4b5f5bce9d2b199d5,
title = "Solving satisfiability problems using field programmable gate arrays: First results",
abstract = "This paper presents an initial report on an innovative approach for solving satisfiability problems (SAT), i.e., creating a logic circuit that is specialized to solve each problem instance on Field Programmable Gate Arrays (FPGAs). Until quite recently, this approach was unrealistic since creating special-purpose hardware was very expensive and time consuming. However, recent advances in FPGA technologies and automatic logic synthesis technologies have enabled users to rapidly create special-purpose hardware by themselves. This approach brings a new dimension to SAT algorithms, since all constraints (clauses) can be checked simultaneously using a logic circuit. We develop a new algorithm called parallel-checking, which assigns all variable values simultaneously, and checks all constraints concurrently. Simulation results show that the order of the search tree size in this algorithm is approximately the same as that in the Davis-Putnam procedure. Then, we show how the parallel-checking algorithm can be implemented on FPGAs. Currently, actual implementation is under way. We get promising initial results which indicate that we can implement a hard random 3-SAT problem with 300 variables, and run the logic circuit at clock rates of about 1MHz, i.e., it can check one million states per second.",
author = "Makoto Yokoo and Takayuki Suyama and Hiroshi Sawada",
year = "1996",
month = "1",
day = "1",
doi = "10.1007/3-540-61551-2_96",
language = "English",
isbn = "3540615512",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "491--509",
editor = "Freuder, {Eugene C.}",
booktitle = "Principles and Practice of Constraint Programming ― CP 1996 - 2nd International Conference, CP 1996, Proceedings",
address = "Germany",

}

TY - GEN

T1 - Solving satisfiability problems using field programmable gate arrays

T2 - First results

AU - Yokoo, Makoto

AU - Suyama, Takayuki

AU - Sawada, Hiroshi

PY - 1996/1/1

Y1 - 1996/1/1

N2 - This paper presents an initial report on an innovative approach for solving satisfiability problems (SAT), i.e., creating a logic circuit that is specialized to solve each problem instance on Field Programmable Gate Arrays (FPGAs). Until quite recently, this approach was unrealistic since creating special-purpose hardware was very expensive and time consuming. However, recent advances in FPGA technologies and automatic logic synthesis technologies have enabled users to rapidly create special-purpose hardware by themselves. This approach brings a new dimension to SAT algorithms, since all constraints (clauses) can be checked simultaneously using a logic circuit. We develop a new algorithm called parallel-checking, which assigns all variable values simultaneously, and checks all constraints concurrently. Simulation results show that the order of the search tree size in this algorithm is approximately the same as that in the Davis-Putnam procedure. Then, we show how the parallel-checking algorithm can be implemented on FPGAs. Currently, actual implementation is under way. We get promising initial results which indicate that we can implement a hard random 3-SAT problem with 300 variables, and run the logic circuit at clock rates of about 1MHz, i.e., it can check one million states per second.

AB - This paper presents an initial report on an innovative approach for solving satisfiability problems (SAT), i.e., creating a logic circuit that is specialized to solve each problem instance on Field Programmable Gate Arrays (FPGAs). Until quite recently, this approach was unrealistic since creating special-purpose hardware was very expensive and time consuming. However, recent advances in FPGA technologies and automatic logic synthesis technologies have enabled users to rapidly create special-purpose hardware by themselves. This approach brings a new dimension to SAT algorithms, since all constraints (clauses) can be checked simultaneously using a logic circuit. We develop a new algorithm called parallel-checking, which assigns all variable values simultaneously, and checks all constraints concurrently. Simulation results show that the order of the search tree size in this algorithm is approximately the same as that in the Davis-Putnam procedure. Then, we show how the parallel-checking algorithm can be implemented on FPGAs. Currently, actual implementation is under way. We get promising initial results which indicate that we can implement a hard random 3-SAT problem with 300 variables, and run the logic circuit at clock rates of about 1MHz, i.e., it can check one million states per second.

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

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

U2 - 10.1007/3-540-61551-2_96

DO - 10.1007/3-540-61551-2_96

M3 - Conference contribution

SN - 3540615512

SN - 9783540615514

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 491

EP - 509

BT - Principles and Practice of Constraint Programming ― CP 1996 - 2nd International Conference, CP 1996, Proceedings

A2 - Freuder, Eugene C.

PB - Springer Verlag

ER -