| Project/Area Number |
23K11214
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 61030:Intelligent informatics-related
|
|---|
| Research Institution | University of Yamanashi |
|---|
Principal Investigator |
鍋島 英知 山梨大学, 大学院総合研究部, 准教授 (10334848)
|
|---|
| Project Period (FY) |
2023-04-01 – 2026-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2025: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2024: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
Fiscal Year 2023: ¥1,820,000 (Direct Cost: ¥1,400,000、Indirect Cost: ¥420,000)
|
|---|
| Keywords | 充足可能性判定（SAT）問題 / 決定的SATソルバー / 並列SATソルバー / 充足可能性判定問題 / 並列処理 / 決定的挙動 / 充足不能証明 |
|---|
| Outline of Research at the Start |
SATは計算機科学における最も基本的かつ本質的な組み合わせ問題であるとともに，ハードウェア・ソフトウェアの検証やプランニング，スケジューリングなど実社会における様々な応用領域の基盤推論技術として幅広く利用されている．複数のCPUや計算機を利用する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技術を利用した他の推論ソルバー，例えば擬似ブール制約ソルバーや解集合プログラミングなどの並列解法においても非同期的な節交換による再現性の欠如という課題があるため，これらに本手法を適用することを検討する予定である．
|
