2016 Fiscal Year Annual Research Report
A Study of Accelerating Boolean Satisfiability Solvers
| 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 |
平成28年度は主として逐次・並列ソルバーの基盤技術となる以下の3つの研究課題に関して取り組んだ．以下にそれらの実績概要を示す．
1. SATソルバーは，その求解過程で無数の学習節を獲得する．学習節の選別は，伝搬速度を維持し，メモリ消費を抑えるため必須の技術である．また拡張融合法の拡張規則や並列ソルバーにおける節交換においても学習節は増加するため，合理的な学習節の選別基準が重要となる．従来手法では，定評のある学習節評価尺度であるリテラルブロック距離を用いて，一定の距離以下または保持上限に達するまで学習節を保持する戦略が一般的であった．我々は，従来手法では伝搬や矛盾を引き起こす節を十分に保持できないことを実証し，問題に依存せず保持上限を定めない戦略として，伝搬や矛盾のカバー率に基づく保持戦略を提案した．この戦略は従来手法よりも高い精度・再現率を示し，求解性能の向上が可能である．
2. 並列SATソルバーではプロセス間の情報交換のタイミングのずれから実行のたびに求解過程が異なる．このためソルバーの評価が難しくなり，効率的な開発を阻害する要因となっている．応用によっては解の再現性が求められる場合もある．そこで並列SATソルバーのための決定的節交換プロトコルについて検討を行った．従来の矛盾回数などの尺度を利用して同期を取る手法では，各プロセスの推論速度が細かく変化する場合に同期待ち時間が多く発生する．そこで通信に一定の遅延を認めることで，待ち時間の削減を図る手法を提案・検討した．
3. 与えられた問題に応じて適切な戦略・ソルバーを選択することは，逐次・並列ソルバーの双方にとって必要な技術となる．与えられたSAT問題に対して深層学習により適したソルバーを選択する手法について改善を図り，SATに特化した前処理を施すことで性能改善が達成できることを実証した．
|
