Takahisa TODA (戸田 貴久)

Offer Organization: Japan Society for the Promotion of Science, System Name: Grants-in-Aid for Scientific Research Grant-in-Aid for Transformative Research Areas (B), Category: Grant-in-Aid for Transformative Research Areas (B), Fund Type: -, Overall Grant Amount: - (direct: 33500000, indirect: 10050000)
本研究では組合せ遷移の実装技術の構築とその産業応用に向けて、研究開発の共通基盤となるソフトウェア開発を目標とする。初年度にあたる本年度は、広く知られているグラフの独立集合の遷移問題（独立集合遷移問題）に対して、4種のアプローチを検討した。1つ目は、組合せ遷移の技法を用いたアルゴリズムの設計であり、主に、状態空間の部分探索の手法を検討した。2つ目は、SAT（充足可能性問題）ソルバーを活用するアプローチである。有限整数領域上の制約を命題論理式へと変換する SAT 符号化を行い、SATソルバーの強力な推論性能を用いて独立集合遷移問題を解くソルバーを開発した。3つ目は、ゼロサプレス型二分決定グラフ (ZDD) を活用するアプローチである。当初予定では、ZDD を上記2手法に援用した高速化を想定していたが、本研究において、ZDD が表す独立集合族を直接遷移させるアルゴリズムの開発に成功したため、ZDD を単独で用いて独立集合遷移問題を解くことが可能になった。4つ目の手法は、当初は予定していない新たな構想であるが、モデル検査と呼ばれる、システムの形式的な検査を可能にする技術を用いた手法である。入力グラフと開始、目標独立集合が与えられた際に、開始集合から目標集合に遷移可能ではないことを検証する記述をモデル検査ソルバーに与え、遷移可能な場合は反例として解となる遷移列を出力する。
以上の4つの技法について、アルゴリズム設計と実装を行った。アルゴリズムの比較実験のためには、適切な入力データが必要であるが、組合せ遷移問題に対する広く知られたベンチマークデータは存在しないため、入力データの作成整備を行った。
配電切替への組合せ遷移技術の適用についても研究を行い、配電切替を全域木遷移問題として定式化し、4つの技法の適用を検討して、実装を行っている。

Offer Organization: Japan Society for the Promotion of Science, System Name: Grants-in-Aid for Scientific Research Grant-in-Aid for Young Scientists (B), Category: Grant-in-Aid for Young Scientists (B), Fund Type: -, Overall Grant Amount: - (direct: 3300000, indirect: 990000)
In this research, we developed an efficient method for computationally hard problems that intrinsically require us to enumerate all solutions of constraint satisfaction problems (CSPs). As a major achievement, we developed a computer-aided method to help us to locate faults in the designs of hardware and software. Model checking is a widely applied method for the verification and debugging of information systems. A counterexample is detected from an erroneous system as a proof of error by executing model checking, however, there is a big gap between computing counterexamples and locating faults. We thus proposed a method for providing information regarding error in a more understandable form than counterexamples by abstracting many counterexamples, which is expected to aid us in moving a trace of failure (i.e., a counterexample) to an understanding of the essence of the failure.
Beside the model checking application, we tackled security/privacy-related researches.

Offer Organization: Japan Society for the Promotion of Science, System Name: Grants-in-Aid for Scientific Research Grant-in-Aid for Young Scientists (B), Category: Grant-in-Aid for Young Scientists (B), Fund Type: -, Overall Grant Amount: - (direct: 2800000, indirect: 840000)
This research project developed practically efficient methods for the following important problems: the minimal hitting set enumeration problem and extended problems such as the dualization of Boolean functions and the all solutions SAT problem.Not only novel methods proposed in this research, but also most major methods proposed before were implemented as public software, and their efficiency and characteristics were confirmed through comprehensive experiments.These results and software are publicly available on our website.
Toward applications to knowledge discovery, our software was applied to itemset mining problems based on the so-called declarative approach in data mining, and experiments using actual data taken from transaction databases were conducted, by which promising research problems in this approach and useful knowledge were obtained.