Solving satisfiability problems using reconfigurable computing

Takayuki Suyama, Makoto Yokoo, Hiroshi Sawada, Akira Nagoya

研究成果: ジャーナルへの寄稿学術誌査読

32 被引用数 (Scopus)


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.

ジャーナルIEEE Transactions on Very Large Scale Integration (VLSI) Systems
出版ステータス出版済み - 2月 2001

!!!All Science Journal Classification (ASJC) codes

  • ソフトウェア
  • ハードウェアとアーキテクチャ
  • 電子工学および電気工学


「Solving satisfiability problems using reconfigurable computing」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。