|
本研究では、重要なNP完全問題の一つとして知られるSAT問題を解くSATソルバの並列化において、対象の問題の構造を考慮することで高速な探索を実現することを目的とする。具体的には、問題に含まれる変数と変数間の関係をグラフとして考え、特定の変数間に存在する強い依存関係(問題の構造)をグラフの構造として抽出し、その構造に対する集中的な探索を並列に行う処理の提案・実装を行う。これにより、従来の並列SATソルバでは回避が困難だった並列ワーカー間での探索空間の重複を意図的に避けることが可能となり、そして問題に内在する構造に対する探索をより加速させることで効率的かつ高速な探索を実現する。
本年度の研究では、SAT問題をグラフに変換して互いに密に関係する変数の集合(コミュニティ)を抽出し、そのコミュニティを利用した手法で主に二つの成果をあげた。一つ目が、並列SATソルバの各ワーカーが異なるコミュニティに対する探索を行う手法であるcommunity branchingを実装したCBPeneLoPeが、SATソルバの性能を競う国際的な競技会であるSAT Race 2015の並列ソルバ部門において4位(著者別で3位)に入賞した。二つ目が、各ワーカーにおいて変数の割り当ての矛盾から学習される学習節のコミュニティ構造を利用した効率的な共有方法の提案である。学習節は探索空間の枝狩りを促進するための有益な情報であるため、ワーカー間で共有することが望ましいが、従来の手法では共有後に使われない学習節が多く存在したため、本提案手法はこの無駄を減らすことで通信量の削減と探索時間の短縮を実現した。
|
