2021 Fiscal Year Research-status Report
A Development of Perfect Sampling with SAT/SMT Solvers
| Project/Area Number |
20K11694
|
|---|
| Research Institution | Hiroshima University |
|---|
Principal Investigator |
岡村 寛之 広島大学, 先進理工系科学研究科(工), 教授 (10311812)
|
|---|
| Project Period (FY) |
2020-04-01 – 2023-03-31
|
| Keywords | シミュレーション / パーフェクトサンプリング / マルコフ過程 / SAT/SMTソルバ |
|---|
| Outline of Annual Research Achievements |
令和3年度は主にMRSPNに対する手法の改良を行った．令和2年度においてMRSPNにおける一般トランジションを位相近似を適用してGSPN化する手法を開発したが，これについて(i)位相近似の効率化，(ii)サンプリングの効率化という二点について改善を検討した．位相近似は一般トランジションの発火遅延を支配する一般を位相型分布と呼ばれる連続時間マルコフ連鎖で記述される分布で置き換えることでMRSPNを指数トランジションならびに即時トランジションからなるGSPNへ近似的に表現する手法である．特に高い近似精度を維持するためには高い次元の位相型分布のパラメータ推定が必要となり，必然的に全体の状態数が爆発的に増加する．この問題に対して，位相構造を特殊化してより効率的な計算で近似を行う手法の検討を行った．また特殊化した位相構造によりSAT/SMTの式を減らす効果があり，全体のサンプリング時間の効率化が実現できた．また，FSPNに対する検討も行った．FSPNは状態を連続時間の微分方程式で記述されるが，パーフェクトサンプリングを適用するためには時間離散，つまり，なんらかの離散化が必要となる．この点に関しての位相型近似のアイデアが利用できないかどうかの検討を行った．結果として，ある種の構造を持つFSPNはMRSPNで書き換えることが可能であるため，MRSPNに対するパーフェクトサンプリング手法を直接適用できることがわかった．
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
令和3年度では MRSPN と FSPN に対するパーフェクトサンプリングについても検討する予定であったが，FSPNの離散化について通常のオイラー法などの単純な手法では誤差が与える影響が非常に大きくサンプリングがうまく行えないことがわかった．これについては，ある種のクラスに限定して位相型近似のアイデアが利用できないかどうかという，当初の計画とは異なる方向からの検討が必要となったため．また，MRSPNに関するツールの開発についても昨今の半導体供給不足により計算環境の構築が遅れたため，令和4年度に開発をずらす必要が生じた
|
| Strategy for Future Research Activity |
令和4年度は，まずMRSPNに対するアルゴリズムのツール化を行う．次に，FSPNで記述されたハイブリッドシステムへの適用を行う．FSPNでは微分方程式を厳密な意味で離散化する必要がある．そのためには可積分系のアルゴリズムの適用と，そのアルゴリズムに対するSAT/SMTによる上下限値の導出が期待される．一方で，令和3年度に検討した連続状態の位相構造による離散化も同時に検討していく．また，マルコフ連鎖モンテカルロ法の一種であるハミルトニアンモンテカルロ法がある種の微分方程式を利用するものであるため，その利用可否についても検討する．
|
| Causes of Carryover |
新型コロナウィルスで予定していた国際会議や国内研究集会が中止やオンライン開催となり，旅費および参加費が少額になったため．次年度使用額は令和４年度に行われる国際会議や研究集会の参加費および計算資源の整備に利用する．
|
