1
戸田研究室 ◇ 概要 人工知能、システム検証、データマイニングなど、 さまざまなところに現れる数理的な問題を解決する 高速ソルバーの研究開発と応用を行っています。 ◇ どんな問題を扱うのか？ 例） 命題論理の充足可能性（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, … • 高次の知的処理の実現 • ネットワーク検証 • データマイニング 計算機環境の例 主メモリ：512GB CPU：インテル Xeon プロセッサ E7-2830 2.13GHz x 4 コア数： 32 キーワード： プログラミング 、アルゴリズム、離散数学
