戸田研究室

◇概要人工知能、システム検証、データマイニングなど、さまざまなところに現れる数理的な問題を解決する高速ソルバーの研究開発と応用を行っています。

◇どんな問題を扱うのか？例） 命題論理の充足可能性（Boolean Satisfiability; SAT）与えられた論理式を真にする命題変数への値割り当てを探索する問題

入力 (x2 ⋁ ¬x3) ⋀ (x1 ⋁ x2 ) ⋀ (¬x1 ⋁ x3)

出力 x1 = 0, x2 = 1, x3 = 0

x1 = 0

x2 = 1

x3 = 0膨大な数の場合分けのため、アルゴリズムを工夫しないと太刀打ちできない！

◇なぜ重要なのか？• 最初にNP完全性が証明された問題あらゆるNP問題はSATに多項式時間で帰着可能

• NP問題の例頂点被覆問題、部分和問題、ハミルトン閉路問題

• 多くの応用論理回路の等価性、有界モデル検査、プランニング、暗号解読

• SAT問題を実用上高速に解くソフトウェア（SATソルバー）の研究が盛ん！

ここを作りたい！

◇高速化の原理• SATは計算困難な問題の典型例

• しかし、実用上高速に問題を解くための各種の計算技法が知られている

• 変数選択• 単位伝搬• 失敗からの学習• リスタート• Lazy データ構造

• ヒューリスティックスを解析する理論研究もある

◇チャレンジ！• 決定問題SATを“超える”問題への挑戦

• AllSAT：解の列挙• ＃SAT：解の個数の数え上げ

• PBSAT：疑似ブール制約の問題

• SMT, QBF, ASP, …• 高次の知的処理の実現

• ネットワーク検証• データマイニング

計算機環境の例主メモリ：512GBCPU：インテル Xeon プロセッサ

E7-2830 2.13GHz x 4コア数：32

キーワード： プログラミング、アルゴリズム、離散数学