2023 Fiscal Year Research-status Report
| Project/Area Number |
23K11214
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
|
|---|
| Project Period (FY) |
2023-04-01 – 2026-03-31
|
| Keywords | 充足可能性判定（SAT）問題 / 決定的SATソルバー / 並列SATソルバー |
|---|
| Outline of Annual Research Achievements |
高速な決定的並列SATソルバーの実現のため，本研究では非共有メモリ環境に対応した大規模な決定的並列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
本研究では2023年度からの３年間にかけて，大きく3つの研究課題に取り組む計画である：(1) 非共有メモリ環境において効率的な決定的並列SATソルバーを実現する手法の検討，(2) 並列SATソルバーにおいて充足不能を効率よく証明する手法の検討，(3) (1)(2) の成果をベースに並列SATソルバーのための汎用フレームワークの実現である．
上記のうち(1)については研究実績の概要で示したように，既存の遅延節交換法の拡張手法について検討するとともに，節交換タイミングの記録手法という再現性のある挙動を担保するための新しい手法を提案している．予備的評価により有効性も確認しており順調に推移している．また(2)(3)は今後２年間で取り組む予定であるが，(2)の充足不能の効率的な検証手法については前述の節交換タイミングの記録手法に基づくアルゴリズムを検討中である．(3) は，(1)および(2)の成果をベースに取り組むため，今後の課題となる．
以上よりおおむね順調に進展していると判断した．
|
| Strategy for Future Research Activity |
課題(1)の非共有メモリ環境における効率的な決定的並列SATソルバーを実現する手法の検討については，引き続きより効果的な遅延節交換の拡張手法および節交換タイミング記録手法について検討を進める．現状はまだ予備的な評価段階であるため，非共有メモリ環境における実装を行い提案手法について詳細な評価を行う．
課題(2)の充足不能証明の効率的な検証方法の実現については，節交換タイミングの記録手法に基づき実現できると考えているため，これまでの知見を生かし効率的な検証のためのアルゴリズムの検討と実装，評価について取り組む．
課題(3)の非共有メモリ環境向けの決定的並列SATソルバーの汎用フレームワークの実現方法としては，遅延節交換法に基づく手法と交換タイミングの記録法に基づく手法の両方が考えられる．いずれの手法についてもこれまで検討を進めてきており，その詳細な評価を行い適切な手法に基づき開発する計画である．
また本研究では主としてSATソルバーにおける効率的な再現性の実現方法を検討しているが，SAT技術を利用した他の推論ソルバー，例えば擬似ブール制約ソルバーや解集合プログラミングなどの並列解法においても非同期的な節交換による再現性の欠如という課題があるため，これらに本手法を適用することを検討する予定である．
|
| Causes of Carryover |
研究発表を行った国内会議の一部について授業等の事情によりオンライン参加したため次年度使用額が生じている．次年度の研究発表費用および研究活動の効率化のために開発環境の拡充費用にあてる予定である．
|
