プラスティック・セル・アーキテクチャの言語処理系に関する研究

2003 Fiscal Year Annual Research Report

• Project/Area Number: 14580380
• Research Institution: Kyushu University
• Principal Investigator: 長谷川 隆三 九州大学, 大学院・システム情報科学研究院, 教授 (20274483)
• Co-Investigator(Kenkyū-buntansha): 越村 三幸 九州大学, 大学院・システム情報科学研究院, 助手 (30274492) ; 藤田 博 九州大学, 大学院・システム情報科学研究院, 助教授 (70284552)
• Keywords: 充足可能性(SAT)問題 / SATソルバ / 探索ヒューリスティクス / 知的バックトラック

Research Abstract

本年度は,充足可能性問題(SAT問題)を解くSATソルバをFPGA上に実装し,実行速度を向上させる方式を幾つか検討した.SAT問題は様々な問題を定式化できる一般的な枠組みとして知られており,この効率的な解法は広く探求されている.SAT問題はNP完全問題なので,実用的な解法には探索ヒューリスティクスを組み込む必要があるが,これは動的な情報に基づいて行われるので,ハードウェア化が困難だと一般的には考えられている.これを打開するために,二つのヒューリスティクスの組み込みを考案し,その効果を測定した.
二つとも探索の分岐の非決定性に着目したもので,一つは先読みを行い一番有望そうな分岐を選択し,もう一つは分岐時点で分岐数の最小の分岐を選択する.前者は,先読みのコストが大きいため小さな問題では性能が劣化してしまったが,大きな問題ではそのコスト以上の性能改善が見られた問題もあった.後者は少ないコストで大きな性能改善が達成できることを実証した.実行時間のみに着目すると,ソフトウェアのソルバに比べ数十倍から数百倍の高速化を確認した.
一方,探索時に発生するバックトラックに着目し,ハードウェア実行可能な知的バックトラック機構(バックトラック時に無駄な探索枝を剪定する手法)を考案し,FPGA上に実装した.内部の状態遷移機械はやや複雑になるものの,探索空間の削減効果を確認した.
以上,実行時間のみに着目すると,ソフトウェアのソルバに比べてFPGA上のソルバは優位である.しかし,ハードウェアの再構成時間(論理合成と配置配線に要する時間)まで含めると優位であるとはいえない.本研究の方式では,問題ごとに再構成を必要とするので,再構成時間までを含めて高速化を図らないと,真に高速化に成功したとはいえない.そこで,今後は再構成時間を短縮する技法を編み出す必要がある.また,ソフトウェアのソルバで一般的に行われている補題の生成機構の組み込みも今後の課題である.

Research Products

• [Publications] 藤田博, 河野真史, 長谷川隆三: "定理証明系PCMGTPのFPGA上の実装について"九州大学大学院システム情報科学紀要. 第9巻第1号(掲載予定). (2004)
• [Publications] Miyuki Koshimura, Megumi Iwaki, Ryuzo Hasegawa: "Minimal Model Generation with Factorization and Constrained Search"情報処理学会論文誌. 第44巻第4号. 1163-1172 (2003)