2015 Fiscal Year Research-status Report
問題の構造を利用した高速並列SATソルバの研究開発
| Project/Area Number |
15K16057
|
|---|
| Research Institution | National Institute of Informatics |
|---|
Principal Investigator |
薗部 知大 国立情報学研究所, ビッグデータ数理国際研究センター, 特任研究員 (50747269)
|
|---|
| Project Period (FY) |
2015-04-01 – 2017-03-31
|
| Keywords | SATソルバ / 並列 / 探索 / グラフ |
|---|
| Outline of Annual Research Achievements |
本研究では、重要なNP完全問題の一つとして知られるSAT問題を解くSATソルバの並列化において、対象の問題の構造を考慮することで高速な探索を実現することを目的とする。具体的には、問題に含まれる変数と変数間の関係をグラフとして考え、特定の変数間に存在する強い依存関係(問題の構造)をグラフの構造として抽出し、その構造に対する集中的な探索を並列に行う処理の提案・実装を行う。これにより、従来の並列SATソルバでは回避が困難だった並列ワーカー間での探索空間の重複を意図的に避けることが可能となり、そして問題に内在する構造に対する探索をより加速させることで効率的かつ高速な探索を実現する。
本年度の研究では、SAT問題をグラフに変換して互いに密に関係する変数の集合(コミュニティ)を抽出し、そのコミュニティを利用した手法で主に二つの成果をあげた。一つ目が、並列SATソルバの各ワーカーが異なるコミュニティに対する探索を行う手法であるcommunity branchingを実装したCBPeneLoPeが、SATソルバの性能を競う国際的な競技会であるSAT Race 2015の並列ソルバ部門において4位(著者別で3位)に入賞した。二つ目が、各ワーカーにおいて変数の割り当ての矛盾から学習される学習節のコミュニティ構造を利用した効率的な共有方法の提案である。学習節は探索空間の枝狩りを促進するための有益な情報であるため、ワーカー間で共有することが望ましいが、従来の手法では共有後に使われない学習節が多く存在したため、本提案手法はこの無駄を減らすことで通信量の削減と探索時間の短縮を実現した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
競技会ではおおむね良い成績を収め、本研究成果を論文として執筆中(一部投稿完了)であるため。
|
| Strategy for Future Research Activity |
より高速な並列SATソルバの実現に向けて、SAT問題の構造を異なる視点からの解析も検討する。また、より大規模な環境に向けての実装にも取り組む。それとともに、国内外の学会に積極的に参加して成果の周知を行う。
|
