Solving satisfiability problems on FPGAs using experimental unit propagation

Takayuki Suyama, Makoto Yokoo, Akira Nagoya

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

3 Citations (Scopus)

Abstract

This paper presents new results on an innovative approach for solving satisfiability problems (SAT), that is, 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. We have developed an algorithm that is suitable for a logic circuit implementation. This algorithm is basically equivalent to the Davis-Putnam procedure with Experimental Unit Propagation. The algorithm requires fewer hardware resources than previous approaches. Simulation results show that this method can solve a hard random 3-SAT problem with 400 variables within 1.6 minutes at a clock rate of 10MHz. 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
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages434-445
Number of pages12
Volume1713
ISBN (Print)3540666265, 9783540666264
DOIs
Publication statusPublished - 1999
Externally publishedYes
Event5th International Conference on Principles and Practice of Constraint Programming, CP 1999 - Alexandria, United States
Duration: Oct 11 1999Oct 14 1999

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume1713
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other5th International Conference on Principles and Practice of Constraint Programming, CP 1999
CountryUnited States
CityAlexandria
Period10/11/9910/14/99

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'Solving satisfiability problems on FPGAs using experimental unit propagation'. Together they form a unique fingerprint.

  • Cite this

    Suyama, T., Yokoo, M., & Nagoya, A. (1999). Solving satisfiability problems on FPGAs using experimental unit propagation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1713, pp. 434-445). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1713). Springer Verlag. https://doi.org/10.1007/978-3-540-48085-3_31