CDCLを勉強する
from 2023-03
CDCLアルゴリズムを勉強する
資料を睨みつけるだけの簡単なお仕事
Conflict-driven clause learning (CDCL) SAT solvers — CS-E3220: Propositional satisfiability and SAT solvers documentation
絵があるの良すぎて理解の速度が5億倍になった
学習節の生成(=DPLL アルゴリズムにおけるバックトラックの一般化みたいなやつ)が Conflict Graph をどうカットするかに帰着される，という認識
解析せずにバックトラックで戻っていたところから、もうちょっとマシな情報としての学習節を得たいという試み
どうやってカットを決めるの？
より短い学習節のほうが少ないレベル(探索の早い段階)で探索を打ち切れる可能性が高いので良さそう
→より decision side の"表面積"が小さくなるようにカットを選びたい
しかしカットの決定にそんなに時間はかけられない……
1つの妥協案として Unique Implication Point なるものを考えるといいらしいです
First UIP cut
たぶん Implication Graph を陽に持つ必要はない
辺はカットの瞬間にのみ意味を持つので，First UIP cut なら decision side の集合のみを管理すればいいはず
カットを決めた後，どこまで戻ればいいのかがわからん
たぶんどこまで戻ってもいいんじゃないか？
学習節は節の線形結合によって求めることができるのでいつでも使える
カットによって定まる Conflict の原因には必ず最新の decision level が含まれる
First UIP cut では
最新の decision level の原因を除いたとき，一番大きなレベルまで戻る
ここで最新の decision level になっているものは1つだけである
Unique Implication Point の定義より明らか
つまりこのレベルは「学習節が単位節になる最小のレベル」であり，戻ると必ず単位伝播が発生する
「より小さいレベルまで戻って早めに方向転換したい，が確実に方向転換できなかった場合戻っただけ損である」という欲求を叶える