2014 Fiscal Year Research-status Report
| Project/Area Number |
26330248
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
鍋島 英知 山梨大学, 総合研究部, 准教授 (10334848)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | 充足可能性判定(SAT)問題 / SATソルバー / 動的簡単化 |
|---|
| Outline of Annual Research Achievements |
平成26年度は主に以下の2つの研究課題に関して取り組んだ．それぞれの実績概要を示す．
1. 軽量動的簡単化手法の拡張
単位伝搬処理から抽出したバイナリ節を基にした軽量簡単化手法の拡張に取り組んだ．具体的には，命題変数の真偽値の同定手法をバイナリ節同士の自己包摂融合の観点から再定式化し，従来手法では検出漏れがあることを明らかにし，網羅的に検出する手法を考案・実装した．また任意の節と，その節内のリテラルを前件に持つバイナリ節群との融合節を高速に求める手法を考案し，一定の条件を満たす場合に変数の真偽値または等価リテラルの同定を行う手法を考案・実装した．またバイナリ節の連鎖関係を一定の範囲で調べ，3つ以上のリテラルの等価性を検出する手法を実装した．評価実験の結果，特に充足不能な問題群に対して性能向上が得られることを確認した．
2. 軽量動的簡単化手法のための頑健なヒューリスティクスの検討
動的簡単化手法では，求解中に冗長な節やリテラルが除去されるが，これがしばしば変数選択ヒューリスティクス等に影響を与え，性能の低下をもたらす場合がある．この影響を緩和し頑健なヒューリスティクスを半自動獲得するための枠組みを検討した．一般にSATソルバーのヒューリスティクス開発では，ヒューリスティクスの考案，効率的な実装手法の実現，多様な問題に対する有効性の評価というサイクルを繰り返し多大な時間を消費する．そこで変数選択ヒューリスティクスを対象として，その開発労力の軽減のためヒューリスティクスの半自動構築手法を検討した．ヒューリスティクスの構成要素はソルバーの開発経験などの知見をもとに9種類を人手で作成し，それらの組み合わせや重み付けをパラメータ調整器により自動発見する．評価実験の結果は求解数において既存の手法を超えるものではなかったが，いくつかのヒューリスティクスが有効となる可能性を持つことを示した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究実績の概要で示した2テーマのうち，「1. 軽量動的簡単化手法の拡張」に関しては，変数の真偽値の同定や3つ以上の等価リテラルの検出など従来手法よりも簡単化能力を強化し，それによる性能向上を確認しており，当初の計画以上に順調に推移している．
また「2. 軽量動的簡単化手法のための頑健なヒューリスティクスの検討」に関しては，当初の計画よりも前倒しして取り組んでいる．SATソルバーの開発においては，変数の真偽値や等価リテラルを同定することで探索空間を削減する手法を導入しても，問題によっては性能が低下することがしばしば発生する．これは変数選択や学習節管理，リスタート戦略などの各種ヒューリスティクスに影響を与えるためであると考えられる．このような不安定さを軽減することは，SATソルバーの高速化技術の開発において極めて重要であると考え，前倒しして研究を進めている．平成26年度は，ヒューリスティクス開発のための基盤システムの構築を行っており，今後も継続して頑健なヒューリスティクスの開発に取り組む予定である．
一方，平成26年度には「3. 拡張融合法に基づく次世代SAT ソルバーの検討」ならびに「4. マルチCPU コアまたはGPU 向けSAT ソルバーの設計」に関しても検討を進める予定であったが，上述のテーマに研究リソースを割いたため，十分に検討を進めることができなかった．
以上より，テーマ1,2に関しては計画以上に進展しており，テーマ3,4に関しては遅れているため，総合的におおむね順調と判断した．
|
| Strategy for Future Research Activity |
平成27年度は以下の3つの課題に取り組む．
1. 頑健なヒューリスティクスの開発：平成26年度に引き続き，SATソルバー内で使用される各種のヒューリスティクスについて検討を進め，多様な問題群ならびに動的簡単化手法に対して頑健なヒューリスティクスの開発に取り組む．平成26年度では変数選択ヒューリスティクスを対象としたが，節管理やリスタート戦略などのヒューリスティクスについても検討を行う．またヒューリスティクスの半自動獲得においては訓練事例の評価時間が大きな課題となるので，その効率化についても検討を行う．
2. 拡張融合法に基づく次世代SATソルバーの検討：拡張融合法における拡張規則は，リテラルの選言と等価な新規命題変数を導入する操作である．拡張規則の適用にあたり，どの時点でどのリテラル群を選択し，別名を与えるのかが問題となる．従来の手法では，主として節群の記述長の削減を指向して拡張規則を適用していた．これは，SAT問題における命題変数や節が，原問題においてどのような変数や制約を符号化したものか基本的には分からないため，構造的な形に着目せざる得ないためである．本研究ではまず，原問題が与えられた場合に，それを符号化したSAT 問題においてどのような変数を拡張対象に選択すれば良いか検討を行う．すなわち構文的な特徴だけでなく，意味的な特徴を取り入れる手法を検討する．
3. マルチCPUコアまたはGPU向けSATソルバーの検討：並列プログラミングのための技術的調査，特にGPU におけるプログラミングモデルの習熟に取り組む．また平行して，並列化を前提としたアルゴリズムを検討する．例えば，一度に複数の変数を選択してそれらの真偽値を仮定することで並列性を高める手法や，複数個の矛盾原因の同時検出と，それらからの並列学習手法について検討を行う．
|
