| 研究課題/領域番号 |
20K11934
|
|---|
| 研究機関 | 山梨大学 |
|---|
研究代表者 |
鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
|
|---|
| 研究期間 (年度) |
2020-04-01 – 2023-03-31
|
| キーワード | 充足可能性判定（SAT）問題 / 決定的SATソルバー / 並列SATソルバー |
|---|
| 研究実績の概要 |
並列SATソルバーにおいて動作の再現性を保証することは，SATの応用や並列ソルバー自体の研究開発にとって重要である．しかし再現性のある動作を保証し，かつ効率的に動作する決定的並列SATソルバーを実現することは容易ではなく，実際多くの並列SATソルバーは非決定的である．我々は，遅延節交換法に基づく決定的並列SATソルバーの構築を支援するフレームワークを開発し，その実装の効率化やアルゴリズムの改善に継続的に取り組んでいる．例えばワーカー間での節交換に要する手間の軽減や，非決定的並列SATソルバーにおいて定評ある節交換戦略の再定式化と導入などである．代表的な複数の逐次SATソルバーに我々のフレームワークを適用し，少ない手間で決定的並列SATソルバーを構築可能であることを示すとともに，非決定的並列SATソルバーに匹敵または超える性能を達成できることを実証している．一般的に決定的並列ソルバーでは節交換において待ち時間が発生するため，非決定的並列ソルバーを超える性能を示していることは興味深い結果であるといえる．
また並列SATソルバーにおける探索の多様性を確保するため，異なる種類の逐次SATソルバーを決定的に並列動作させる手法についても検討を進めている．同一のソルバーを並列動作させていた場合は抑えられていた同期のための待ち時間が大きく増大することが課題であり，その低減案の検討を進めている．
並列SATソルバーにおいては各ワーカーが与えられたSAT問題のコピーを持つため，多数コア環境においてはメモリ消費量が問題となる．そこで逐次SATソルバーにおいて，SAT問題中に出現する規則的な構造を活かして圧縮し，それを展開することなく解くことでメモリ消費量を抑え，また圧縮時に抽出した規則的な構造の情報をもとに圧縮前よりも高速に解く手法を考案し，評価を進めている．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究では決定的並列SATソルバーの高速化ならびに高機能化に向けて，次の6つの研究課題に取り組んでいる：(1)遅延学習節交換法の精錬，(2)多様性と集中性のバランスをとる探索戦略の検討，(3)多数CPUコア環境における学習節交換戦略の検討，(4)インクリメンタルSATや充足不能コア抽出機能等の実現，(5)多数CPUコア環境におけるメモリ削減手法の検討，(6)決定的並列 SAT ソルバーの構築を支援するフレームワークの検討．
上記のうち，(1) は2020年度にソルバーの各処理の実行時間を詳細に見積もることでどこまで待ち時間を低減できるのか示している．(2) は異なる種類のSATソルバー群を効率的に並列動作させる方法について現在検討を進めており，今後も継続予定である．(4) はインクリメンタルSATにおける再現性を保証するアルゴリズムの考案・実装はできており，今後 (6) のフレームワークに適用する予定である．(5) はベースとなる逐次ソルバーにおいて与えられたSAT問題を圧縮し，省メモリかつ高速に解く手法を考案・評価している．(6) は昨年度から継続的に改良を実施しており，非決定的並列SATソルバーに匹敵する性能を実現できることを示している．以上からおおむね順調に進展していると判断した．
|
| 今後の研究の推進方策 |
決定的並列SATソルバーは挙動の再現性を保証するために同期待ちが発生するため，その必要がない非決定的並列SATソルバーを超える性能を達成することは難しいと考えていた．しかし我々が開発したフレームワークを複数の代表的逐次SATソルバーに適用して構築した決定的並列SATソルバーはいずれも良好な性能を示している．また研究開発の過程より，決定的並列SATソルバーでは新しい戦略・ヒューリスティクスの評価や性能のチューニングが再現性の保証により非常に容易となっており，並列SATソルバーを今後研究開発する上でその基盤となりうると考えている．
そこでこのフレームワークをベースとして，発展的に研究開発を進めることが重要であると考え，多数CPUコア環境における学習節交換戦略を中心に研究を進める．これには異なる種類の逐次SATソルバーにおける学習節交換における待ち時間の抑制も含まれる．これまでに評価した学習節交換戦略の中では，HordeSAT で提案された常に一定量の情報を交換する戦略がよい結果を示しているが，この知見をベースとして決定的並列SATソルバーにおける学習節交換戦略について検討を進める．
|
| 次年度使用額が生じた理由 |
研究発表を行った国内・国際会議がCOVID-19感染対策のためオンライン開催された．このため旅費を次年度にまわしている．旅費の一部はオンライン発表のための機材導入や，研究活動の効率化のために評価用計算機クラスタを増枠し，その利用負担金に充てる予定である．
|
