2010 Fiscal Year Annual Research Report
超高性能自動推論システムのための高抽象度機能素子に関する研究
| Project/Area Number |
22650028
|
|---|
| Research Institution | Kyushu University |
|---|
Principal Investigator |
藤田 博 九州大学, システム情報科学研究院, 准教授 (70284552)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
長谷川 隆三 九州大学, システム情報科学研究院, 教授 (20274483)
越村 三幸 九州大学, システム情報科学研究院, 助教 (30274492)
|
|---|
| Keywords | FPGA / Verilog / SATソルバー / MGTP |
|---|
| Research Abstract |
本年度は、従来技術における最新の状況と課題について調査した。具体的には、自動推論における主要な3つの機能である(A)単位伝播、(B)照合・単一化、(C)探索及び確率論的手法を研究項目とし、調査を行った。特に、FPGA上のSATソルバーPCMGTPに関して再検討を行った。その結果、以下の諸点について確認するとともに、いくつかの新たな知見を得た。
・全般的な事項:FPGAのようにメモリを基本要素として、所望の機能を関数表の形で実現する原理に基づく素子、およびそのためのVerilog処理系等の開発環境においては、ビット演算に基づいた最適と考えられるデザインが必ずしも奏功しない場合がある。むしろ、整数演算等に特化されたマクロ回路を組み合わせる方が効果的である。
・単位伝播:連鎖的な単位伝播を1クロック内に実行する組合せ回路が原理的に可能だが、これをFPGAによって実装するのは現実的でない。この目的には、より原始的、すなわちゲートレベル、もしくはトランジスタレベルの再構成可能素子が望ましい。
・照合・単一化:変数や部分構造の多重出現に関して、DAG構造を直接的に回路化する方法、ならびに、ストリームプログラミングの手法に準じた方法等が効果的である。包摂検査に対しても同様である。これらにつき、並列プログラムによるシミュレーションによって確認した。
・探索及び確率論的手法:各種SATソルバーやMGTP処理系、最適化処理系等を試作し、実験データを収集して傾向を分析した。SWARM法をベースにしたハイブリッド探索の有効性等を確認した。
|
