2020 Fiscal Year Research-status Report
| Project/Area Number |
20K11934
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
|
|---|
| Project Period (FY) |
2020-04-01 – 2023-03-31
|
| Keywords | 充足可能性判定（SAT）問題 / 決定的SATソルバー / 並列SATソルバー |
|---|
| Outline of Annual Research Achievements |
再現可能な動作を保証する決定的並列SATソルバーの高速化のために，遅延学習節交換法の精錬化に取り組んだ．遅延学習節交換法では，各ソルバーの求解動作を一定間隔のピリオドで区切り，スレッド間のピリオド差が一定の範囲内であれば待ち時間なく学習節を交換する．これを効率的に動作させるためには，各ソルバーにおける各ピリオドの実行時間をできる限り等しくし，かつそれを再現可能な指標に基づき実現する必要がある．我々は，ソルバーのソースコードにおけるブロック（複合文）ごとの実行回数を算出し，その値から実行時間を推定する手法を提案・実装した．従来の矛盾回数やリテラルアクセス回数に基づく手法は実装しやすいもののピリオドの実行時間には大きなずれが生じていた．本手法は実装に手間はかかるものの，ピリオドの実行時間を高精度で推定することが可能である．実際に我々の開発した決定的並列SATソルバーは，2020年度に開催された国際SAT競技会の並列ソルバー部門において３位に入賞している．この部門に参加した14種類の並列ソルバーのほとんどは決定的動作を保証しておらず，我々のソルバーが３位に入賞できたことは，決定的動作を担保しつつも無駄がない効率的なアルゴリズムを実現できたことを実証している．
また決定的並列SATソルバーを少ない手間で構築するための汎用的フレームワークについても検討を行った．非決定的並列SATソルバーのフレームワークと同様に入力節の登録，学習節の輸入・輸出用のインターフェイスに加え，再現可能な動作を実現するためにピリオド更新処理の定期的実行とメモリアクセス回数のカウント処理を追加したフレームワークの設計・実装を行った．このフレームワークを利用することで，おおよそ300行程度のコードを追加するだけで逐次SATソルバーを決定的並列SATソルバーに組み込むことが可能となることを確認した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究では次の6つの研究課題に取り組む予定である：(1)遅延学習節交換法の精錬，(2)多様性と集中性のバランスをとる探索戦略の検討，(3)多数CPUコア環境における学習節交換戦略の検討，(4)インクリメンタルSATや充足不能コア抽出機能等の実現，(5)多数CPUコア環境におけるメモリ削減手法の検討，(6)決定的並列 SAT ソルバーのための汎用的枠組みの検討．
上記のうち(1)および(6)は研究実績の概要で述べたように一定の成果を挙げている．(6)の汎用的フレームワークに関する詳細な性能評価や性能改善に向けた取り組みは今後も継続予定である．また(4)のうちインクリメンタルSATについてもすでにアルゴリズムの検討は完了しており，今後(6)の汎用的フレームワークにおいて実現予定である．この他に(5)についても，逐次SATソルバーを対象としてSAT問題を圧縮したまま解くことでメモリ使用量を抑制する手法についても検討を行っている．以上よりおおむね順調に進展していると判断した．
|
| Strategy for Future Research Activity |
遅延学習節交換法を精錬化することで，決定的並列SATソルバーであっても最新の非決定的並列ソルバーに迫る性能を達成可能であることを確認したが，効率的な遅延学習節交換法の実現には大きな開発の手間を要する．これを改善するため決定的並列SATソルバーの構築を容易にする汎用フレームワークについて検討を進めており，当初考えていたよりも少ない手間で実現できることを確認した．並列SATソルバーのベースとなる逐次SATソルバーは絶えず進化しているため，このような汎用フレームワークを研究開発することは，SATに関する研究分野だけでなく応用分野にとっても有益であることを改めて認識した．本研究では，今後以下に示した並列SATソルバーの高速化・高機能化のための研究開発に取り組むが，これらを特定のソルバー上にのみ実装するのではなく，汎用フレームワーク上で実現可能にすることも同時に検討を進めるものとする．
(1)多数CPUコア環境におけるメモリ削減手法の検討：ポートフォリオ型並列SATソルバーでは，各ソルバースレッドがそれぞれ節集合を保持するため，多数のCPUコア環境または大規模なSAT問題では並列実行数を抑える必要がしばしば生じる．我々は逐次SATソルバーを対象としてSAT問題を圧縮したまま解くことでメモリ使用量を抑制する手法について研究を進めており，これを並列SATソルバーにも適用することを検討する．
(2)決定的並列ソルバーにおける充足不能コア抽出手法の検討：充足不能の原因を表す充足不能コア抽出は応用分野においてしばしば求められる機能であり，決定的並列SATソルバー上でこれを効率よく実現する手法について検討を進める．また充足不能コア抽出だけでなく，インクリメンタルSATなどについて汎用フレームワーク上でこれらの機能を提供することを検討する．
|
| Causes of Carryover |
研究発表を行った国際会議・国内会議がCOVID-19感染対策のためオンライン開催された．このため令和２年度の旅費を次年度にまわしている．令和３年度もオンライン開催が主となる見込みのため，令和２年度および３年度の旅費の一部はオンライン発表のための機材導入に充てる予定である．
|
Research Products
(3 results)
