2017 Fiscal Year Research-status Report
大規模制約充足問題の全解探索のための実用的な計算基盤の確立とその応用
| Project/Area Number |
17K17725
|
|---|
| Research Institution | The University of Electro-Communications |
|---|
Principal Investigator |
戸田 貴久 電気通信大学, 大学院情報理工学研究科, 助教 (50451159)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | モデル検査 / アルゴリズム / SAT / 制約 |
|---|
| Outline of Annual Research Achievements |
AllSATソルバーの高速化手法についてまとめた学術論文「Exploiting Functional Dependencies of Variables in All-Solutions SAT Solvers」が論文誌に採録された。
現在、AllSATの応用研究として有界モデル検査の拡張を進めている。有界モデル検査は（ハードウェアやソフトウェアなど）システムの誤りを発見する手法である。実用的なモデル検査器（例えば、NuSMV2）の内部処理では、SATソルバーが呼び出され、誤りの探索を行う。もし誤りが発見されたときには、モデル検査器は、システムの内部状態がどのように遷移したときに違反状態に陥るのかを表す実行シーケンスを返す。ここまではモデル検査器が自動で処理してくれるが、この実行シーケンスから誤りを引き起こした根本原因を特定する部分は通常人手が必要である。
実行シーケンスは長く複雑なので人間が理解するのは困難であり、過去の研究でその負担を軽減する仕組みが提案されてきたが、まだ十分には手が付けられていないのが現状である。そこで、本研究では、AllSATソルバーをモデル検査器のコア技術として用いて、多数の実行シーケンスを生成することができるように拡張した。さらに、特定の変数の値を固定して実行シーケンスを生成する「制約による絞り込み機能」など、人手による解析を補助する機能を開発した。現在、予定している機能実装は終了し、論文の執筆にとりかかっている。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
本研究の基本アイディアを当該分野の標準的なソフトウェアを拡張する形で実装した。
このソフトウェアは３０万行程からなる巨大なものであり、その根本の部分から手を加える必要があったので、大量のコードを理解して、追加機能のコードを追加するのに想定以上に時間がかかってしまった。しかし、予定していた機能の実装はほぼ終了して、現在は論文執筆に取り掛かっている。
|
| Strategy for Future Research Activity |
まずは、これまでの研究成果を論文にまとめあげることが第一である。これで計算基盤がひとまず完成したことになる。今後はこの枠組みをネットワーク検証における問題解決につなげていくことを計画している。
|
| Causes of Carryover |
計算機の故障や不具合などなかったので、当該年度に新しい計算機を購入していなかったが、次年度は購入を検討している。
|
