2017 Fiscal Year Annual Research Report

A Large-scale Enumeration of Minimal Hitting Sets And Its Application to Knowledge Discovery

Research Project

Project/Area Number	26870011
Research Institution	The University of Electro-Communications
Principal Investigator	戸田貴久電気通信大学, 大学院情報理工学研究科, 助教 (50451159)
Project Period (FY)	2014-04-01 – 2018-03-31
Keywords	アルゴリズム / 論理関数 / SAT / モデル検査 / 列挙
Outline of Annual Research Achievements	本研究では、決定グラフと呼ばれるデータ構造を用いて、網羅的な計算問題に対する実用的な計算技法の開発を目指している。本研究課題の中核として位置付けている「論理関数の双対化」、「All Solutions SAT問題」に取り組み、さらにそれらを土台にして、モデル検査への応用に向けて取り組んだ。論理関数の双対化は、論理式の表現形式の変換の一種であり、昔からよく研究されてきた基本的な問題である。本研究では、決定グラフを用いた計算手法を開発して、誰でも利用できる形で公開した。次に、All Solutions SAT問題（AllSAT問題）に取り組んだ。AllSAT問題は、与えられた命題論理式のすべての充足解を求める問題である。SATソルバーが様々な産業応用に役立てられている一方で、その派生問題のAllSATは十分に研究されていないことに着目し、本研究ではAllSAT問題を効率的に解く手法を開発し、それを応用に役立てるための計算基盤を確立した。本研究で実装したプログラムや利用したデータセットはすべて、誰でも利用できる形で公開している。現在、AllSATの応用研究として有界モデル検査の拡張を進めている。有界モデル検査はシステムの誤りを発見する手法である。実用的なモデル検査器（例えば、NuSMV2）の内部処理では、SATソルバーが呼び出され、誤りの探索を行う。もし誤りが発見されたときには、モデル検査器は、システムの内部状態がどのように遷移したときに違反状態に陥るのかを表す実行シーケンスを返す。実行シーケンスは長く複雑なので人間が理解するのは困難であり、過去の研究でその負担を軽減する仕組みが提案されてきたが、まだ十分には手が付けられていないのが現状であった。そこで、AllSATソルバーをモデル検査器のコア技術として用いて、多数の実行シーケンスを生成することができるように拡張した。