2018 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 |
平成30年度は主に以下の3つの研究課題に関して取り組んだ．それぞれの実績概要を示す．
1. 探索の無駄を低減するヒューリスティクスの検討：並列SATソルバーでは各ソルバースレッドの探索空間の集中性と多様性のバランスをとることが重要となる．そこで他ソルバーから輸入した学習節の使用率と重複率に基づき探索状況の集中性・多様性を評価する手法とそれに基づく変数選択ヒューリスティクスの制御方法について検討を行った．4コア環境における予備的な評価実験の結果，本手法によって求解数が若干向上することを確認した．
2. 対称性に基づく動的な簡単化手法の検討：対称学習節の生成による同様の証明の繰り返しを避ける手法では，しばしば対称学習節の候補数が膨大となる．これを抑制するため，対称学習節の使用率に着目し，あまり使用されない対称学習節を生成する要因となる対称性を除外することで候補節数を大幅に削減し，それにより速度向上が達成できることを実証した．また，対称性伝搬と動的簡単化を組み合わせる手法について検討し，等価リテラルがこれまでよりも多く検出可能になることを示した．評価実験により，対称性伝搬の処理コストのため求解時間は増加するものの，求解にかかるステップ数を大きく削減できることを確認した．
3. 多数コア環境における決定的並列SATソルバーの性能改善：多数CPUコア環境での排他制御の待ち時間と同期待ち時間を低減するため，輸出用学習節集合を交換間隔ごとに用意することで排他制御を減らすとともに，交換間隔のさらなる精密化や，スレッド間で探索状況が大きく乖離することを抑制するための学習節の強制適用手法などを考案し，64CPUコアからなる環境であっても非決定的ソルバーに匹敵する性能を示すことを実証した．
|
| 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. 探索の無駄を低減するヒューリスティクスの検討」は，H29年度に逐次型ソルバーについて検討し，H30年度に並列型ソルバーについて検討し，それぞれ一定の成果を達成している．このテーマについては計画通り順調に進展しており，R元年度も引き続き研究を継続する予定である．「2. 対称性に基づく動的な簡単化手法の検討」についても，対称学習節手法および対称性伝搬と動的簡単化の組み合わせ手法の双方について一定の成果を達成しており，順調に推移している．「3. 多数コア環境における決定的並列SATソルバーの性能改善」は，本研究課題における技術評価のための基盤ソルバーの性能改善の取り組みであり，多数コア環境においても非決定的ソルバーに匹敵する性能を獲得できたことは大きな成果である．一方，H30年度に予定していた「4. 証明木の生成コスト低減手法の検討」については動的簡単化における証明木のコスト低減について検討を進めている段階であり，予定よりも遅れている．
以上より，テーマ1,2に関してはおおむね順調であり，テーマ3は計画以上に進展しており，テーマ4は遅れているため，総合的におおむね順調と判断した．
|
| Strategy for Future Research Activity |
令和元年度は以下の課題に取り組む．特に進捗が遅れている「2. 拡張融合法のための実用的な適用条件の検討」については研究代表者と大学院生を割り当て進展を図る．
1. 探索の無駄を低減するヒューリスティクスの検討：SATソルバーの基本戦略の1つであるリスタートは，探索状況の改善を目的として探索をやり直すヒューリスティクスである．これまでにリスタートしても状況が改善しない場合がしばしばあること，および，その発生要因となる決定変数の頻出パターンが存在することがわかっている．この決定変数の頻出パターンを求解中に高速に求めるため，近似オンライン頻出パターンマイニングアルゴリズムの導入を検討する．その後，リスタート後の変数選択ヒューリスティクスに対してバイアスをかけ，探索状況の改善を積極的に図る手法について検討する．
2. 拡張融合法のための実用的な適用条件の検討：拡張融合法を用いることで証明が短縮可能な条件について検討を行う．またその適用条件を効率的に判定するための手法についても検討する．これまでに検討してきた長さ2のバイナリ節群に対する適用条件では，学習節の獲得をストリームデータの発生源と見なし，頻出アイテムを近似抽出するオンライン型マイニングアルゴリズムによって拡張対象のリテラルペアを高速に抽出する手法を考案している．そこで新しい適用条件についても同様の高速な手法が活用できないか検討する．
|
