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

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Solving satisfiability problems using field programmable gate arrays: First results'. Together they form a unique fingerprint.

Cite this