2017 Fiscal Year Research-status Report
| Project/Area Number |
17K00300
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
|
|---|
| Project Period (FY) |
2017-04-01 – 2020-03-31
|
| Keywords | 充足可能性判定（SAT）問題 / SATソルバー / ヒューリスティクス / 動的対称性除去 |
|---|
| Outline of Annual Research Achievements |
平成29年度は主に以下の3つの研究課題に関して取り組んだ．それぞれの実績概要を示す．
1. 探索の無駄を低減するヒューリスティクスの検討：SATソルバーの基本戦略の1つであるリスタートは，探索状況が悪くなった際にその改善を目的として探索をやり直すヒューリスティクスであり，最新のソルバーでは高頻度でリスタートが実行されている．我々はリスタートをしても探索状況がしばしば改善されないことを実験的に示し，その発生要因となる決定変数の頻出パターンが存在することを示した．今後，そのような決定変数の選択を抑制する手法を検討する予定である．
2. 対称性に基づく動的な簡単化手法の検討：対称性除去は論理式に存在する対称性を持った構造に対し，その探索を制限する制約を追加することで同様の証明の繰り返しを避ける手法である．対称性除去手法の1つに求解中に獲得した学習節の対称的な節を生成することで，矛盾の対称パターンの発生を防ぐ手法があるが，しばしば多数の対称学習節を追加するため，逆に求解のオーバーヘッドとなることがある．我々は，学習節の質と対称学習節の使用頻度の間に強い相関があることを示し，質の悪い学習節からの対称学習節の生成を抑制する手法を実装し，評価実験により求解数の若干の向上が達成できることを確認した．
3. 決定的並列SATソルバーの開発：並列SATソルバーは学習節を互いに交換することで証明の短縮を図る手法である．しかし，ほとんどの並列SATソルバーは実行のたびに求解時間が異なるなどの非決定的な振る舞いをする．そこでソルバー間の同期間隔の精密化と遅延学習節交換手法によってソルバー間の待ち時間を大きく削減する手法を考案し，評価実験により決定的でありつつも最新の非決定的並列SATソルバーに匹敵する性能を持つことを実証した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
研究実績の概要で示した3テーマのうち，「1. 探索の無駄を低減するヒューリスティクスの検討」は，計画ではH30,31年度に予定していたテーマであるが，それを前倒しして進めており，計画以上に進展しているといえる．リスタート戦略における無駄の発生要因が存在することを示したことは今後の改善のための重要な基盤となると考えられる．「2. 対称性に基づく動的な簡単化手法の検討」については対称学習節の生成による対称性除去手法のコスト低減について検討し，若干ではあるものの性能向上を達成している．今後は対称性伝播手法に基づく動的簡単化についても検討を進める予定であり，本テーマの進捗はおおむね順調であるといえる．「3. 決定的並列SATソルバーの開発」は，本研究課題における技術評価のための基盤ソルバーとして開発したものであり，最新の非決定ソルバーに匹敵する性能を達成できたことは大きな成果である．一方，H29年度に予定していた「4. 証明木の生成コスト低減手法の検討」については動的簡単化における証明木のコスト低減について検討を進めている段階であり，予定よりも遅れている．
以上より，テーマ1,3に関しては計画以上に進展しており，テーマ2はおおむね順調，テーマ4は遅れているため，総合的におおむね順調と判断した．
|
| Strategy for Future Research Activity |
平成30年度は以下の課題に取り組む．
1. 探索の無駄を低減するヒューリスティクスの検討：探索状況が改善しないリスタートの要因となる決定変数の頻出パターンを求解中に高速に求めるため，近似オンライン頻出パターンマイニングアルゴリズムの導入を検討する．その後，リスタート後の変数選択ヒューリスティクスに対してバイアスをかけ，探索状況の改善を積極的に図る手法について検討する．
2. 対称性に基づく動的な簡単化手法の検討：対称性伝播ではある部分真偽値割当ての下で成り立つ対称性から真偽値を伝播することで無駄な探索を抑制する．一方，我々がこれまで提案してきた動的簡単化では，頻繁に実行される単位伝播処理から抽出されるリテラル間の含意関係を利用する．これらの手法を組み合わせることで相乗的な効果が期待できるため，この手法について検討・評価を行う．
3. 拡張融合法のための実用的な適用条件の検討：拡張融合法を用いることで証明が短縮可能な条件について検討を行う．またその適用条件を効率的に判定するための手法についても検討する．これまでに検討してきた長さ2のバイナリ節群に対する適用条件では，学習節の獲得をストリームデータの発生源と見なし，頻出アイテムを近似抽出するオンライン型マイニングアルゴリズムによって拡張対象のリテラルペアを高速に抽出する手法を考案している．そこで新しい適用条件についても同様の高速な手法が活用できないか検討する．
|
