拡張融合法を用いた高速SATソルバの研究開発

2018 Fiscal Year Research-status Report

• Project/Area Number: 17K12742
• Research Institution: National Institute of Informatics
• Principal Investigator: 薗部 知大 国立情報学研究所, ビッグデータ数理国際研究センター, 特任研究員 (50747269)
• Project Period (FY): 2017-04-01 – 2020-03-31
• Keywords: SATソルバ / 探索

Outline of Annual Research Achievements

本研究では、NP完全問題の一つとして知られるSAT問題を解くSATソルバに対して、従来の基盤アルゴリズムである融合法より強力と考えられている拡張融合法を、問題の構造を考慮して適用することで、より高速な探索の実現を目指す。拡張融合法は探索中に新たな変数を導入する手法であり、本研究では問題をグラフとしてとらえ、そのグラフのコミュニティ構造やページランクに着目することで、問題の構造をとらえた変数の導入を行う。
本年度の研究では、本研究の成果から得られた情報をもとに改良を加えた並列SATソルバCBPeneLoPeとCCSPeneLoPeが、SATソルバの性能を競う国際的な競技会であるSAT Competition 2018の並列SATソルバ部門において、それぞれ5位と6位に入賞した。

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

本研究の成果である並列SATソルバが競技会で概ね良い順位に入賞し、関連論文を執筆中であるため

Strategy for Future Research Activity

拡張融合法の対象となる新たな変数の導入は、問題の構造をグラフとしてとらえる手法以外に、探索中に判明する、SATソルバの探索に関わる各種パラメータの値も考慮することで、より効果的な変数の発見を見込んでいる。その成果のソルバ競技会への参加、および国内外への論文投稿を予定している。

Causes of Carryover

国際学会への参加が少なく、また購入を予定していたマシンの性能を抑えたため。次年度は成果の報告および情報集のために学会への参加を積極的に行う予定である。