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