2022 Fiscal Year Annual Research 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 |
令和4年度ではアルゴリズムの高速化を行った．SAT/SMTソルバに基づいたアルゴリズムでは一般化確率ペトリネット（GSPN）の各トランジションに対してSAT/SMTソルバで解くべき式を導出し，各ステップにおいてそれを解くことで状態の上下限を求める手法を行っていた．この際に，GSPNのPインバリアント条件に基づく式も同時にSAT/SMTソルバに渡されるようになっている．これらは状態に対する必要条件を与えており，一部のGSPNではこれらの条件を与えないとパーフェクトサンプリングが収斂しないため必要な式となる．しかしながら，従来の手法ではこれらをすべて利用していたため，この必要条件に関する式が膨大になりアルゴリズムの計算量が増加する一因となっていた．一方，これらは上下限を与えるための必要条件であるため，必ずしもすべての式を使わなくても良い．いくつかの必要条件を省いた場合，上下限値の幅は大きくなるものの，収斂した場合のアルゴリズムの正しさは保証される．この原理とGSPNの局所性，つまり発火するトランジションの周辺のプレースしか状態が変化しないことに着目してアルゴリズムの高速化を行った．具体的には，トランジション毎にPインバリアント条件から得られる必要条件を入力および出力プレースに関係したものだけに限定した．この改善により最大10000倍の高速化が実現できた．
研究機関を通じて，SMTソルバによるパーフェクトサンプリング手法が確立された．特に大きな成果として(i)一般化確率ペトリネットに適用できるようなアルゴリズムの拡張と，(ii)高速化が挙げられる．これらを達成したことにより手法の汎用性が大幅に向上し，実用的な問題に対して適用することが可能となった．
|
Research Products
(4 results)
