| 講演名 | 2004/1/16 モデル生成型定理証明器のFPGA上の実装(FPGAとその応用及び一般) 河野 真史, 藤田 博, 長谷川 隆三, |
|---|---|
| PDFダウンロードページ | PDFダウンロードページへ |
| 抄録(和) | 本論文では,定理証明器PCMGTP(Propositional Constraint Model Generation Theorem Prover)のFPGA(Field Programmable Gate Array)上での実装と評価について述べる. PCMGTPは,与えられた命題論理の節集合の充足可能性を,健全かつ完全に決定するモデル生成法に基づいている。節集合が与えられると, PCMGTPカーネルモジュールの一部と共に,全体の回路がFPGAのチップ上で再構成される.PCMGTPでは確定節を用いた閉包計算に最も多くの時間を要することから,閉包計算部分の設計に可能な限りハードウェアの並列性を利用することが不可欠である.また,場合分けに最適な節を選択したり,証明探索の際のバックトラックを行う回路も設計する.いくつかの充足可能性問題のベンチマークに対する実験の結果,非常に短い実行時間で問題を解くことができた. |
| 抄録(英) | In this paper, a design and implementation of theorem prover PCMGTP on an FPGA chip is described. PCMGTP is based on a model-generation method which is sound and complete to decide satisfiability of a set of clauses of propositional logic. Given a set of clauses, the whole circuit is re-configured on an FPGA chip together with a small PCMGTP kernel modules. Since closure computation with definite clauses is most time consuming in PCMGTP, it is essential to exploit as much hardware parallelism as possible in designing the corresponding part. Also some useful circuits are designed to choose suitable clauses for case splitting and to perform backtracking for proof search. Experimental results show significant performance in solving some benchmark SAT problems. |
| キーワード(和) | 定理証明器 / モデル生成 / SATソルバ / FPGA / リコンフィギュラブルコンピューティング |
| キーワード(英) | Theorem provers / Model generation / SAT solvers / FPGA / Reconfigurable computing |
| 資料番号 | VLD2003-134,CPSY2003-43 |
| 発行日 |
| 研究会情報 | |
| 研究会 | VLD |
|---|---|
| 開催期間 | 2004/1/16(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | VLSI Design Technologies (VLD) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | モデル生成型定理証明器のFPGA上の実装(FPGAとその応用及び一般) |
| サブタイトル（和） | |
| タイトル（英） | Implementing a Model-Generation Theorem Prover on an FPGA |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 定理証明器 / Theorem provers |
| キーワード(2)（和/英） | モデル生成 / Model generation |
| キーワード(3)（和/英） | SATソルバ / SAT solvers |
| キーワード(4)（和/英） | FPGA / FPGA |
| キーワード(5)（和/英） | リコンフィギュラブルコンピューティング / Reconfigurable computing |
| 第 1 著者 氏名（和/英） | 河野 真史 / Atsushi KAWANO |
| 第 1 著者 所属（和/英） | 九州大学大学院システム情報科学研究院 |
| 第 2 著者 氏名（和/英） | 藤田 博 / Hiroshi FUJITA |
| 第 2 著者 所属（和/英） | 九州大学大学院システム情報科学研究院 |
| 第 3 著者 氏名（和/英） | 長谷川 隆三 / Ryuzo HASEGAWA |
| 第 3 著者 所属（和/英） | 九州大学大学院システム情報科学研究院 |
| 発表年月日 | 2004/1/16 |
| 資料番号 | VLD2003-134,CPSY2003-43 |
| 巻番号（vol） | vol.103 |
| 号番号（no） | 579 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |