Solving satisfiability problems using logic synthesis and reconfigurable hardware

Takayuki Suyama, Makoto Yokoo, Hiroshi Sawada

Research output: Contribution to journalConference articlepeer-review

14 Citations (Scopus)

Abstract

This paper presents new results on an 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). This approach becomes feasible due to the recent advances in FPGAs and high-level logic synthesis. In this approach, each SAT problem is automatically analyzed and implemented on FPGAs. We have developed an algorithm which is suitable for implementing on a logic circuit. This algorithm is equivalent to the Davis-Putnam procedure with a powerful dynamic variable ordering heuristic. The algorithm does not have a large memory structure like a stack; thus sequential accesses to the memory do not become a bottleneck in algorithm execution. Simulation results show that this method can solve a hard random 3-SAT problem with 400 variables within 20 minutes at a clock rate of 1 MHz.

Original languageEnglish
Pages (from-to)179-186
Number of pages8
JournalProceedings of the Hawaii International Conference on System Sciences
Volume7
Publication statusPublished - 1998
Externally publishedYes
EventProceedings of the 1998 31st Annual Hawaii International Conference on System Sciences. Part 1 (of 7) - Big Island, HI, USA
Duration: Jan 6 1998Jan 9 1998

All Science Journal Classification (ASJC) codes

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Solving satisfiability problems using logic synthesis and reconfigurable hardware'. Together they form a unique fingerprint.

Cite this