2020-06-17
情報科学特別演習 の打ち合わせ第5回
（今回は #延長戦 で、一時間半ぐらいやってた）
handbook p103 definition 3
状況
Handbook of Knowledge Representationを読んでいた
議題
Definition 3 の確認
resolution proof では、証明の木ではなく、証明過程の節の列で証明を表すことが多い
例: 入力 $ (a \lor b) \land (\lnot a) \land (\lnot b)
$ (a \lor b), \lnot a, b, \lnot b, \bot
ランダウの記号($ \omega(f(n))は何を表すのか質問した)
SAT の相転移
Ising モデルと関係があるらしい
統計力学の概念を利用した SAT ソルバがあるらしい
survey propagation
survey inspired decimation
Restart, 変数選択に関すること
鍋島先生によるスライド
http://www-erato.ist.hokudai.ac.jp/docs/seminar/nabeshima.pdf
http://atrg.jp/ja/index.php?plugin=attach&pcmd=open&file=20141015-atos10.pdf
計算モデルに関する本(これは SAT ソルバの話ではないが、流れでこの話になった)
https://www.amazon.co.jp/dp/4000103520
計算モデルへの招待
機械モデル
関数モデル(帰納的関数
ラムダ計算)
論理モデル
書換えモデル
代数モデル
CDCL の実装をするにあたって、どの Learning scheme がいいのか？
1UIP が典型的らしい
やりたいこと
CDCL 実装
#情報科学特別演習 #diary