[2E3-OS-13b] AIと制約プログラミング(2/3)

[2E3-OS-13b-01] SIR感染症モデルに対するブール式を用いた有界モデル検査

〇花田 研太¹ (1. 奈良先端科学技術大学院大学)

キーワード：新型コロナウィルス、感染症モデル、SIRモデル、有界モデル検査、充足可能性判定問題

新型コロナウィルスを始めとした感染症の脅威は人類社会に影響を及ぼし続けており，感染症に関する研究は非常に重要である．感染症を数理モデルで表す方法として微分方程式を用いた確率的モデルであるSIR (Susceptible-Infected-Recovered) モデルがある．このモデルは重要な性質を数理的に証明することが出来る一方，確率パラメータが現実と乖離していた場合は意味の無い結果になってしまう恐れがある．
本研究は，ブール式を用いた確率を全く考慮しないSIRモデルを定式化し，有界モデル検査を用いて解析する手法を提案する．有界モデル検査とは，システムが望ましい状態へ有限時間内に到達可能かを検査する手法であり，モデルの状態を記号的に表現することでシステムが取り得る全ての状態を表し，起こりうる全ての可能性を網羅的に検査する．従って，状態遷移がどのような確率分布に依存しているかは全く関係が無い．
本研究ではパンデミックの収束時間を求めるアルゴリズムを検討し，ワクチンの供給量がどの程度感染症伝播を抑制するかをSMTソルバーを用いて数値的に評価した．