2020-07-01
状況
議題
監視リテラルを調べる
とてもわかりやすい✅
（以降、本筋とはあまり関係がないが先生が最近注目しているソルバの話）
機械学習を使ったソルバの高速化
SAT: boolean satisfiability, boolean constraint satisfiability problem (bCSP)
命題変数への割当で論理式を充足するものを求める
SMT: satistiability modulo theories
一階述語論理
pCSP: predicate constraint satisfiability problem
二階述語論理
述語変数が出てくる世界
述語変数への割当で論理式を充足するものを求める
そもそも述語変数とは：引数を持つ命題変数
命題変数の型 : bool
n引数述語変数の型: T1 -> … -> Tn -> bool
sum(x,y) が y が 0 から x の話を表す
sum : int -> int -> bool
制約
sum(0,0) ∧
forall x,y,z.(sum(x,y) <= x > 0 ∧ sum(x-1,z) ∧ y = z + x) ∧
forall x,y.(y >= x <= sum(x,y))
sum(x,y) |-> y >= x は制約を満たすか？
1つ目 sum(0,0) ≡ 0 >= 0 OK
3つ目 forall x,y.(y >= x <= y >= x) OK
2つ目 forall x,y,z.(y => x <= x > 0 ∧ z >= x-1 ∧ y = z + x) OK
解の候補: sum(x,y) |-> y>=0
3つ目の制約を満たさない
反例: y = 0, x = 1
(0 >= 1 <= sum(1,0))
ここから、学習節のように ¬sum(1,0) が導かれる
（今はありえないが）学習節が矛盾したら UNSAT
sum(1,0) と ¬sum(1,0) が出てきたりしたらダメということ
学習節を満たすような解の候補は無限にある
どうやって解の候補を選ぶ？
=> 解の template を用いる
例: sum の解の template は ax + by >= c where a,b,c は未知の係数
一般には任意個の ∧ や ∨ を使う必要がある
ax + by >= c ∧ dx + ey >= f ∨ …
たとえば総和の公式には累乗が現れるわけだが、そういうことを考えると多項式を含む template も考える必要が出てくるかもしれない
実際、このようなことをするときは単純な template からより複雑な template を考えていくようになる。しかしながら、そのような template も無数にあるわけで、これらをどのように選ぶのかを機械学習を用いた結果効率的なソルバが作れたという話があった、とのことだった。
来週は先生が忙しいので打合せがない可能性が高い。