| 講演名 | 2005-01-25 FPGA上に実装されたPCMGTPを用いたSAT問題の解決(応用1, FRGAとその応用及び一般) 木之下 昇平, 松田 純一, 藤田 博, 越村 三幸, 長谷川 隆三, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 本論文では, FPGA上に実装された定理証明器PCMGTP(Propositional Constraint Model Generation Theorem Prover)の改良と評価について述べる.PCMGTPは一階述語論理のCMGTPを命題論理に限定したものであり, ハードウェア化に適している.我々が以前実装したPCMGTPを詳細に検討した結果, プログラム上のデータ表現や, 推論エンジンの状態数等に冗長な部分を発見した.それらを改善し, 新たにBCBE回路の導入や, トーナメント回路の改良を行うことにより, SATソルバ全体の回路規模の大幅な削減や, 実行時間の短縮を図ることができ, 様々な充足可能性問題に対する実験で優れた実行結果を得ることができた. |
| 抄録(英) | In this paper, a new design of the SAT solver PCMGTP implemented on an FPGA chip is described. Although the previous implementation of PCMGTP achieved considerable speedup in solving SAT benchmark problems compared to the software counterpart of MGTP, it failed to compete with the state-of-the-art SAT solvers in speed and was unable to deal with large problems due to the limited capacity of FPGA. We tried to improve our design by removing some redundancy in the data representation and the redundant states in the deduction engine. Also, we developed a new circuit called BCBE for performing logical implication, and modified the tournament circuit so as to deal with very large candidates and to shorten the critical path. As the result, the new implementation achieved speedup by factor of five as well as an order of magnitude space reduction compared to the previous one. |
| キーワード(和) | SATソルバ / 再構成可能論理デバイス / 定理証明 / モデル生成法 |
| キーワード(英) | SAT solvers / FPGA / Reconfigurable logic / Theorem proving / Model generation |
| 資料番号 | VLD2004-107,CPSY2004-73 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2005/1/18(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | FPGA上に実装されたPCMGTPを用いたSAT問題の解決(応用1, FRGAとその応用及び一般) |
| サブタイトル（和） | |
| タイトル（英） | Solving SAT problems by PCMGTP on FPGA |
| サブタイトル（和） | |
| キーワード(1)（和/英） | SATソルバ / SAT solvers |
| キーワード(2)（和/英） | 再構成可能論理デバイス / FPGA |
| キーワード(3)（和/英） | 定理証明 / Reconfigurable logic |
| キーワード(4)（和/英） | モデル生成法 / Theorem proving |
| 第 1 著者 氏名（和/英） | 木之下 昇平 / Shohei KINOSHITA |
| 第 1 著者 所属（和/英） | 九州大学大学院システム情報科学府 Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University |
| 第 2 著者 氏名（和/英） | 松田 純一 / Junichi MATSUDA |
| 第 2 著者 所属（和/英） | 九州大学大学院システム情報科学府 Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University |
| 第 3 著者 氏名（和/英） | 藤田 博 / Hiroshi FUJITA |
| 第 3 著者 所属（和/英） | 九州大学大学院システム情報科学研究院 Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University |
| 第 4 著者 氏名（和/英） | 越村 三幸 / Miyuki KOSHIMURA |
| 第 4 著者 所属（和/英） | 九州大学大学院システム情報科学研究院 Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University |
| 第 5 著者 氏名（和/英） | 長谷川 隆三 / Ryuzo HASEGAWA |
| 第 5 著者 所属（和/英） | 九州大学大学院システム情報科学研究院 Department of Intelligent Systems, Graduate School of Information Science and Electrical Engineering, Kyushu University |
| 発表年月日 | 2005-01-25 |
| 資料番号 | VLD2004-107,CPSY2004-73 |
| 巻番号（vol） | vol.104 |
| 号番号（no） | 589 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |