2016 Fiscal Year Annual Research Report
Development of Fast Parallel SAT Solvers Using Problem Structure
| 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ソルバCBPeneLoPeが、SATソルバの性能を競う国際的な競技会であるSAT Competition 2016の並列ソルバSAT問題部門において3位に入賞した。また、CBPeneLoPeをベースに機械学習の手法を応用したCCSPeneLoPeが同部門の2位に入賞した。そして、SATソルバの探索において重要な技術の一つである節学習に関して、学習される節の評価方法に関して研究を行った。探索中に学習される節は探索空間の枝刈りに役立つものの、その全てを保持し続けることはメモリを圧迫することになるため、その一部を削除することが望ましいとされている。その際に使用される節の評価方法に関して、多くのSATソルバで使用されている評価尺度の改良を行い、より効率的な探索を実現した。本成果はIEEE International Conference on Tools with Artificial Intelligence (ICTAI) 2016に採択された。
|
