| 研究概要 |
近年ハードウェアを用いることで,ソフトウェア版SAソルバにおける逐次実行の部分を効率的に並列処理し,より高速に解を求めるSATソルバが開発されるようになってきている.なおSAT問題は,NP完全であることが示された最初の問題で,多くの難問がSAT問題に還元できることが分かっている.我々も,一階述語論理の定理証明系CMGTPを命題論理に限定した,PCMGTP(Propositional Constraint Model Generation Theorem Prover)を開発し,それをFPGA上に実装してきた.しかし,詳しく検討を行ったところ,データ表現方法や,推論エンジンの状態数等に冗長な部分を発見した.本研究では,従来のPCMGTPに改良を加え,FPGA上へ実装した.
具体的には,次のような改良を施した。データ表現において,各変数の付値準位をbit幅で表現していたが,それを整数表現に変更し,レジスタの数を大幅に削減した.また,推論エンジンにおいては,以前の実装の10状態を6状態に削減することに成功した.さらに,BCBE(Burning Candle at Both Ends)回路を新たに導入し効率的なimplicationの実装が可能となった他,未決定リテラルの少ない非ホーン節を決定するトーナメント回路を多クロック化することによってクリティカルパスを短縮することができた.
実験の結果,従来のPCMGTPと比較して回路素子利用効率が約10倍,実行速度については最大動作周波数を約3倍にすることができ,推論エンジンの冗長性の削除と合わせ約5倍の高速化に成功した.またソフトウェアのCMGTPと比較しても,実行時間については数百倍〜数千倍の高速化を実現した、特にN王妃問題においては,論理合成時間を含めてもハードウェアの方が数百倍高速に解を求めることができた.このように回路合成時間を考慮しても,証明時間に膨大な時間を費やす大規模な問題においてはハードウェアが優位であることが示された.
|
