| Project/Area Number |
14580380
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
計算機科学
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
HASEGAWA Ryuzo Kyushu University, Graduate School of Information Science and Electrical Engineering, Professor, 大学院・システム情報科学研究院, 教授 (20274483)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
FUJITA Hiroshi Kyushu University, Graduate School of Information Science and Electrical Engineering, Associate Professor, 大学院・システム情報科学研究院, 助教授 (70284552)
KOSHIMURA Miyuki Kyushu University, Graduate School of Information Science and Electrical Engineering, Research Associate, 大学院・システム情報科学研究院, 助手 (30274492)
|
|---|
| Project Period (FY) |
2002 – 2004
|
| Project Status |
Completed (Fiscal Year 2004)
|
| Budget Amount *help |
¥2,600,000 (Direct Cost: ¥2,600,000)
Fiscal Year 2004: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2003: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2002: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| Keywords | SAT Solver / Model Generation Method / Davis-Putnam Method / Parallel Processing / Hardware Description Language / FPGA / BCBE Circuit / SAT問題 / SATソルバー / 定理証明システム / 推論エンジン / ソフトウェアのハードウェア化 / トーナメント回路 / 充足可能性(SAT)問題 / 探索ヒューリスティクス / 知的バックトラック / 制約充足問題 / ソフトウェア / ハードウェア / 8王妃問題 / 準群の存在問題 / 制約違反の検査 |
|---|
| Research Abstract |
We studied the design and implementation of a SAT-solver on an FPGA chip. While there are many SAT-solvers implemented in software, we aimed to improve the solver's performance by making a machine that solves SAT problems directly.
The machine was described by the Verilog HDL hardware description language and programmed onto a FPGA chip. It performs the model generation method with some modifications that enhance its performance. We achieved high speed by parallel executions of value propagation and satisfiability tests. However, we lost space efficiency because every formula is represented by a sequential circuit and each formula is connected to other formulas via combinatorial circuits. In spite of this inefficiency, experimental results show significant performance gains in solving some benchmark SAT problems
In order to improve space efficiency, we refined this early design. We found much redundancy in data representation and states of the inference engine, etc. Thus, we tried to eliminate the redundancy by (1)decreasing the number of registers by modifying the representation method of prepositional varaible's state, (2)decreasing the number of states of the inference engine from 10 to 6, (3)introducing the BCBE(Burning Candle at Both Ends) circuit for efficient implication, and (4)shortening the critical path by dividing the tournament circuit which chooses a prepositional variable for case splitting. Experimental results show that the new implementation outperforms the old one with regard to both execution time and circuit size.
|
