研究紹介

研究の概要

情報処理の効率化を実現する計算法(アルゴリズム)や関連する数理構造の研究を行っています。 制約充足や最適化など各種の技法を活用して、現実の課題の解決に向けた応用にも取り組んでいます。

研究事例の紹介

制約充足問題

計算機で処理される計算にはさまざまな種類がありますが、そのうち、○○○および△△△およびという条件(制約)をすべて満たすことができるか?もしできるならばその解を求めよ!というようなものがあります。 これを制約充足問題と呼びます。 ちょっと雑な言い方ですが、制約として特徴付けることができるならば、ほぼあらゆる問題は制約充足問題となります。 制約充足問題は人工知能における重要な研究対象のひとつとみなされています。 制約充足問題を効率的に解くための解法やそれを様々な計算に応用する方法など、これまで多くの研究の蓄積があります。

これまでの多くの研究では解を1つ求めることが考えられていましたが、それだけでは不十分なことがあるので、当研究室ではたくさんの解やすべての解を求める方法について研究を進めています。 例えば、全体的な傾向や特徴を把握したいときにはできるだけ多くの解があると助かります。 すべての解を求めることが難しい場合には、全体の代表となるような解ができるだけたくさん欲しくなります。 このときには、偏りがないように無作為に選ぶ必要があるでしょう。 解の一覧ではなくて、単に解の個数だけが知りたいときもあります。 厳密な個数でなくても良いので、その代わりに可能な限り高速に個数の近似値を求めたいときもあります。 このようにさまざまな派生問題があります。

モデル検査

モデル検査は、ハードウェアやソフトウェアの検証に用いられる手法です。 内部状態が時間とともに非決定的に変化するシステムが、仕様通りに動作することを検査できます。 もし仕様に違反する動作が起こりうるならば、そのような動作例がモデル検査の結果として返されます。 この動作例は仕様に対する反例と呼ばれます。 反例は、システムのモデルにおける不具合を特定するための手がかりとなります。 反例を自動的に計算できるため、モデル検査はとても役に立つ手法ですが、反例から不具合箇所を特定することは簡単ではありません。 通常は、人手により反例を検査して、経験や直感などに頼って不具合箇所を何とか特定する以外に手はありません。 そこで、当研究室では、誤りが生じている状況を解析して、不具合箇所の特定に役に立つ情報を計算する方法について研究を進めています。

アイテムセットマイニング

顧客の購買履歴データを活用して、例えば、パンとバターを買う人は牛乳も買いやすい、というような顧客の購買傾向を解析する計算の枠組みがあります。その中で、頻繁に購入される商品の組み合わせを列挙することが重要なタスクの1つです。これを制約充足問題としてモデル化し、制約充足問題の解探索に帰着する方法について研究を進めています。