2020-06-10
情報科学特別演習 の打ち合わせ第4回
状況
Handbook of Knowledge Representation, On the power of clause-learning SAT solvers as resolution enginesを読んでいた
unit propagation & resolution
resolution とは導出規則のひとつで、(C ∨ l) と (D ∨ ¬l) から (C ∨ D) が出るということ
2つの節から新しい節ができた
subsumption とは、包含規則のことで、Wikipediaを見ると……
包含規則（subsumption rule）
ある節 C の全てのリテラルが他の節 D に含まれていれば、それらの節 D を除去する。
議題
On the power of clause-learning SAT solvers as resolution engines がよくわからなかった
CLR だとどのような CNF に対しても多項式オーダーで収まるような証明が生成されることが保障されていることの論文らしい
ここでの証明というのは、Implication graph のこと？
Handbook of Knowledge Representationを読みすすめた
#情報科学特別演習 #diary