| 研究概要 |
命題論理式の充足性を判定するSATソルバは応用分野も広く,すでに優秀なソフトウェアが数多く開発されている.本研究では,ソフトウェア版SATソルバのハードウェア化による高速化を目指した.
従来から我々が研究してきたモデル生成法をハードウェア化することにし,これにDavis-Putnam法(多くのSATソルバが基づいている解法)のアイディアを取り入れて,効率化を図った.ハードウェア化の利点は,並列実行による高速化が狙えることにある.命題変数の値の伝播や各論理式の充足可能性の判定が並列に行える計算機構の設計を行い,それをハードウェア記述言語により実装し,FPGA上で動作実験を行った.
初期の版(旧方式)は,15年度中頃から動作し始め,15年度の終わりには,ほぼ安定的に動作するようになった.この版は,ソフトウェアのソルバに比べて格段に高速化が図れたが,小さな問題でも回路規模が非常に巨大になるという問題を抱えていることが判明した.この問題点を解決するために,詳しく検討を行ったところ,データ表現方法や,推論エンジンの状態数等に冗長な部分を発見した.そこで旧方式のものに改良を加えた(新方式).
具体的には,次のような改良を施した.データ表現において,各変数の付値準位をbit幅で表現していたが,それを整数表現に変更し,レジスタの数を大幅に削減した.また,推論エンジンにおいては,以前の実装の10状態を6状態に削減することに成功した.さらに,BCBE(Burning Candleat Both Ends)回路を新たに導入し効率的なimplicationの実装が可能となった他,未決定リテラルの少ない非ホーン節を決定するトーナメント回路を多クロック化することによってクリティカルパスを短縮することができた.
実験の結果,旧方式と比較して回路素子利用効率が約10倍,実行速度については最大動作周波数を約3倍にすることができ,推論エンジンの冗長性の削除と合わせ約5倍の高速化に成功した.また,回路合成時間を考慮しても,証明時間に膨大な時間を費やす大規模な問題においてはハードウェアが優位であることを示した.
|
