2020-12-16

仮で途中まで作ってみたスライドを見ていただいた。

有界モデル検査：ハードウェアの論理回路など（フィードバックがないものについて）を SAT の論理式で表現できるようになるので、そのシステムが望ましい性質が成り立っているか（仕様を論理式で記述）について判定できるようになる。

k 回展開しても仕様の展開をして大丈夫だったが、k + 1回目だとダメだったりする

様々な拡張などをすることによって、これ以上展開しなくてもバグが発生しない（仕様の違反に辿りつかない）ということを示せたりする

解集合プログラミング：Prolog などでのある問題を解決するためのパラダイムのこと、流行っている？

スライドの改善点

SAT の説明のところで具体的な入力と出力を掲載する

数独については、エンコード前とその後についても掲載する

SAT ソルバーの代表的なアルゴリズム

DPLL, CDCL を並列に並べるのではなく、「DPLL の拡張が CDCL で、代表的なものが CDCL である」と書く

「拡張として節の学習を追加することで探索の効率化をした」

他にも様々なアルゴリズムがある

確率的なやつ

survey inspired decimation

SAT の問題を多項式で表して、多項式のための最適化アルゴリズムで山を見つけてくるとそれが解になる

「SAT competition で優勝している主要なアルゴリズムは CDCL である」など

「可視化」とあるので、図を出しながら説明したい

可視化の意味として「CDCL がわかりづらく、デバッグしにくい」「他の人への説明が難しい」など

聞き手がなんとなくでも CDCL の仕組みがわかったかのような感じの発表になると目的が達成されている

SAT の問題がそもそも難しいという話も入れる

NP 完全

多項式時間アルゴリズムがあるかどうかがそもそもわかっていないが、おそらくない（P ≠ NP）

ナイーブな方法として真理値表を書くことができるが、それでは全然ダメであることを伝える

SAT solver の応用としてどれぐらいの大きさ（節、変数の個数）の問題を解くのかを伝える

最先端の solver がどれぐらいの規模のものを扱えるのか sat competition のページから得る

聞き手にとってはそのような具体的な数値の情報はうれしい

「これぐらいの数独のサイズでも全然真理値表を書いていては間に合わない」など

理論的にも応用的にも難しいとわかると聞き手も興味を持ってくれるかも

応用から導入する？

「SAT solver のアルゴリズム」までに SAT solver のアルゴリズムの重要性を伝えたい（2分ぐらい？）

DPLL を図を用いながらどのように処理が進むのか説明する（ここまで4分くらい？）

節学習が breakthrough であったことを伝える（最も大事な heuristics）

これが非常によく効くので今回採用したということを、実行時間のグラフを出しながら説明

これの動作原理が複雑であり、解説も少ないので「可視化」に意味がある（←動機の再掲）

「今から4分間で皆さんに節学習を理解させてみます」的なことを……

節の学習は具体例と図による説明をする

必要な説明

implication graph

DPLL でもやっている（Unit Propagation, 変数選択）

↑これの可視化もできる

それぞれがグラフを「育てていく」

backtrack

implication graph で最後に選択した変数の真偽選択を反転してやりなおす

これもグラフを見せる

CDCL のアイデアは implication graph 上で矛盾が生じたときの backtrack のやり方が違うということ

矛盾が起きた後の implication graph のカット

矛盾の原因を探している（←これ自体がカットで表現される）

カットに対応する論理式は「これらが出てきてしまったがために conflict が発生した」もの

カットには decision literal 側のものが入っていることを伝える

ある変数の真偽の選択を間違えたから conflict が発生した可能性がある

間違えた選択をやり直すためには、そのカットを表す論理式の否定を節としてソルバーに追加する

これによって同じような探索のミスを繰替えさないようにする

↑これらのハイレベル、具体的な話をする

細かいところは省略、大まかに

/icons/hr.icon

具体的にスライドに入れたいこと