| 研究課題/領域番号 |
23K10998
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60020:数理情報学関連
|
|---|
| 研究機関 | 広島大学 |
|---|
研究代表者 |
岡村 寛之 広島大学, 先進理工系科学研究科(工), 教授 (10311812)
|
|---|
| 研究期間 (年度) |
2023-04-01 – 2026-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2025年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
2024年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2023年度: 1,690千円 (直接経費: 1,300千円、間接経費: 390千円)
|
|---|
| キーワード | シミュレーション / パーフェクトサンプリング / ペトリネットモデル / SAT/SMTソルバ / MtMDD / 確率モデリング / マルコフ連鎖 / モデル検証 |
|---|
| 研究開始時の研究の概要 |
本研究はSAT/SMTソルバによるパーフェクトサンプリング手法の実用化を行う．パーフェクトサンプリングとはマルコフ連鎖の定常解に従うサンプルを厳密にサンプリングする手法であり，数理的には無限時間のシミュレーションを有限時間で実行することに対応する．これはモデルの検証・評価において非常に強力な性質となる．SAT/SMTソルバを用いたパーフェクトサンプリング手法は超多状態システムに対しても適用できる手法であるが，実行速度や検証可能なモデルの制限なの問題点がある．本研究では，SAT/SMTソルバに与える式の簡略化と，準定常解と呼ばれる一般的な解を利用した拡張によりこれらの問題点の解決を目指す．
|
| 研究実績の概要 |
令和5年度はサンプリング手法の効率化を行った．これまでの研究成果から，SAT/SMTに与える制約式を減らすこと（制約式の簡略化）により大幅なサンプリング時間の短縮が実現できていたが，制約式の簡略化のもう一つの効果として，上下限を求める式が短くなるため，総当たり的な手法によりSAT/SMT問題を解くよりも速く解が得られる可能性が考えられた．そこで，簡略化された制約式を使った上下限問題の解集合をあらかじめMtMDD (Multi-Terminal Multi-path Decision Diagram) と呼ばれるコンパクトな表現を用いて，事前に解くことで高速化を図った．MtMDD は多値関数を木によって表現する手法であり，関数内の共通部分を共有化することで多くの組み合わせを持つ入力に対する出力をコンパクトに表現できる．MtMDDは各トランジション毎に作成する必要があるが，一度作成すると，サンプリングを通じて変更することなく利用できるため，解を得るために非常に効率が良い．さらに，簡略化された問題に対しては一つのトランジションあたり，概ね10個程度のノードで問題の解集合を表現できる．解はMtMDDに対する深さ優先探索で簡単に得ることができる．結果として，令和4年度の成果と比較して，最大 100倍程度の高速化が実現できた．これにより，10の200乗状態のモデルに対するパーフェクトサンプリングが 1 秒以内で実施することができ，十分実用に耐え得る速度が実現できた．一方で，MtMDD表現を用いることにより，サンプリング速度が悪化するモデルも存在したため，今後はそのようなモデルに対する効率的なアプローチを模索する．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
計画では令和5年度は吸収状態を持つモデルに対する扱いを行い，令和6年度にサンプリングの改良を行う予定であったが，令和5年度にサンプリングの改良を実施し，十分な成果が得られた．令和6年度以降で，吸収状態の扱い等の実用化における諸問題を扱っていく予定としている．
|
| 今後の研究の推進方策 |
令和6年度以降は，課題として残っている MtMDD による高速化ができないモデルの扱い，吸収状態を持つモデルに対する準定常解を求めるパーフェクトサンプリング，状態縮約の応用を行う予定としている．特に MtMDD による高速化ができないモデルの原因として，Pインバリアントによる制約式が関係していることがわかっている．具体的には，一つの制約式が多くの変数を含む場合に MtMDD が肥大化し，それが高速化を阻害する原因というところまで解明できている．そのため，線形計画法におけるスラック変数のような冗長な変数を導入することで，MtMDDの肥大化を抑える方法について検討する．
|
