今日は融合情報学特別講義に東工大の福永アレックス先生がいらっしゃった.
福永先生とはサービスロボットのプログラム合成について,共同研究させていただいている.
今日は,ロボットとは関係なくSATに関する講義であった.
簡単に言うと,SATとは与えられた論理式の値を真とする論理変数の真偽の組を求める問題である.この問題を世界で一番効率よく解くアルゴリズム(非厳密法)がどうなっているか,という話であった.驚くべきことに,それはコンピュータが自動的に合成したアルゴリズムなのである.
90年以前は厳密法といって,必ず解が求まる手法についての研究が主であったが,93年にGSATという非厳密法が提案されて以来,一気に非厳密法の研究が花開いた.それまでは計算時間の問題で30程度の変数が限界であったが,GSATは一桁多い変数の問題も解くことができたという.
GSATは完全な貪欲法に基づく手法であった.
翌年には
といった要素を取り入れた手法が現れた.
その後は,"貪欲性", "履歴", "ランダムネス"という三つの要素をいかに組み合わせるか,ということがアルゴリズム開発の主題となる.
GSATを開発した研究者は100個ほどのアルゴリズムを提案し,テストしてみてやっと改善の見込まれるアルゴリズムにたどり着いたという.これは,アルゴリズムを見るだけでは,たとえその道の第一人者でも,その良し悪しを見分けることは難しいということである.
それならば,組み換え作業と実験を自動化して,よいものを取り出せばよいのではないか,というアイデアに福永先生はたどり着いた.
具体的には,"貪欲性", "履歴", "ランダムネス"という三つの要素を表現できるプログラム断片(関数など)を定義し,それらを合成する方法(遺伝的プログラミング)を実装した.
結果としては,WalksatやNovelty+といった人手で作られた優れたアルゴリズムに勝る性能を示した.
提案手法の紹介に加えてSATがなぜ重要か,SAT研究者とのやり取り,SATの解法の歴史など背景がしっかり描かれていて非常に面白く聞かせていただいた.
講義の後に,研究室のメンバーと福永先生で白菜鍋と餃子で飲み会をした.
この時のために,西巣鴨のファイト餃子で4パック80個の生餃子を購入してきた.柏や野田のホワイト餃子の技術提携店で,見た目も味もホワイト餃子と近い餃子だった.
飲み会では,調理担当として焼き餃子,水餃子,とり皮揚げ,ねぎ焼き,豚肉としいたけの( 塩炒め|味噌炒め),豚汁(豆板醤入り)などを作った.豚肉料理が多いのは,鍋の残りをつかったためである.
久しぶりに,同じものを何度も作ってると,だんだんうまく作れるようになっていっておもしろい.
昨年卒業した先輩に料理の非常に上手な方がいらっしゃったが,やっぱり料理ができるとすごいなぁと改めて尊敬した.メインの料理を作りつつ,並列にサラダとか酢の物とかの副菜をさっと作れるようになりたいな,と.