A Development of Perfect Sampling with SAT/SMT Solvers

2022 Fiscal Year Final Research Report

• Project/Area Number: 20K11694
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60020:Mathematical informatics-related
• Research Institution: Hiroshima University
• Principal Investigator: Okamura Hiroyuki 広島大学, 先進理工系科学研究科(工), 教授 (10311812)
• Project Period (FY): 2020-04-01 – 2023-03-31
• Keywords: シミュレーション / パーフェクトサンプリング / マルコフ過程 / SAT/SMTソルバ

Outline of Final Research Achievements

In this research, we developed a highly versatile perfect sampling algorithm using SAT/SMT solvers. Perfect sampling is a method drawing samples from the stationary distribution of a Markov chain exactly. The coupling from the Past (CFTP) method is known as one of the representative method of perfect sampling. Perfect sampling is mathematically interesting because it provides a framework for simulating an infinite-time Markov chain in finite time. In this research, we proposed an algorithm to automatically extract formulas to be solved by SAT/SMT solvers for Markov chain models described by stochastic Petri nets or generalized stochastic Petri nets, and generate samples that exactly follow the stationary distribution. Furthermore, we also proposed a method to enhance the computational time, which is a weakness of conventional perfect sampling algorithms, and achieved a speedup of nearly 10,000 times in practice.

Free Research Field

情報学

Academic Significance and Societal Importance of the Research Achievements

パーフェクトサンプリングアルゴリズムは無限時間を有限時間で厳密にシミュレートするための手法であり，その応用範囲はシミュレーションによるシステム性能評価だけでなく，機械学習に対する学習アルゴリズム等への利用など多岐にわたる．これまでのアルゴリズムは実用面については特殊な構造を持つ確率過程にしか適用できなかったが，本研究ではモデルの数理的な構造を自動的に抽出することで，かなり多くのモデルに対して汎用的に利用できるアルゴリズムを開発した．