すごくわかりやすい
コンピュータは1か0で動いていて、1か0を変数とするand, or, not で組み合わせた式を命題論理式とかブール式とか言うんですが、これがすべての基本。コンピュータのLSIの設計はブール式だし、NPと呼ばれる様々な分野の問題(もちろん暗号系も含まれる)もブール式の充足性問題に帰着されます。
a∧b, a∨¬b
とかね。こんな簡単なものが、ほとんどあらゆるものの基本だと言うのが凄い。問題は変数が多い時に難しくなります。千とかは既に当り前らしい。
BDDは命題論理式を最大共有された二分木で表すもので、ZDD は0に向かうノードを省略するもの。BDDは同じノードに向かうものを省略するので、BDDは対称で、ZDDは非対称な問題に向いてます。モデル検証とかにさんざん使われました。その辺りが90年代の認識だったんですが…
ブール式は集合演算でもある。aとかは「aがある」とか読むわけ。そして数百万の要素の集合を圧縮して表示できるということになると、商品管理とかの方の応用が盛り上がったらしい。
で、Knuth 先生のあれに載って、それから大きな予算が付いてという、
基礎研究での超サクセスストーリー
http://www-erato.ist.hokudai.ac.jp/
ということになったらしいです。Zero supress BDD で ZBDD と呼んでいたんですが、Knuth 先生がいけてないから ZDD にしろと言ったらしいです。
重複を許す集合を表す Seq BDDは20年ぶりに発見されたんだけど、Suffix Tree の最大共有と同じものだと。でも、そこに演算を定義できるのが画期的だと言うのを BDD 側から発見できたらしい。これも、
非常に簡単な構造が Break Through になる
という例だと思う。きっと、まだまだ、そういう見落としがある。単にライブラリを使うだけでなく、その基本に立ち戻るのが常に必要だね。
BDD は、もう普通の技術で自分でもライブラリ持っていたりするけど、手抜きなのをスライド見ながら発見したり。久しぶりにいじってみるか。
＊ ＊ ＊ ＊
ソフトウェア科学会全国大会は無事終了しました。当日の運営の方が、その前までのメールのやりとりよりも楽に感じました。運営と言うのはそうあるべきだな。最終日、亀山さんにぶち切れていたのを目撃した人も多いかも :-p まぁ、反省を活かして来年の人には楽をしてもらいたいと思います。
受け付けにいるよりも、発表聞いて質問している方が多かった。まぁ、それが正しい学会の参加の仕方だな。
いろんな人に迷惑かけました。いろいろありがとうございました。
No comments:
Post a Comment