nandaro

SAT ソルバの探索アルゴリズムの根幹とも言えるのが DPLL アルゴリズム。
DPLL とはアルゴリズムを提唱した4人の名前を繋げたもの (Davis-Putnam-Logemann-Loveland) の略。
ググってみた感じだと解説記事は多いので、さらっとだけ触れることにする。

まず DP アルゴリズムというのが 1960 年に提唱された。
全ての節に resolution を適用して単位節を導きながら命題論理式を解いちゃおうというもの。

1962 年に提唱された DPLL アルゴリズムは DP アルゴリズムのマイナーチェンジのようなもので、resolution の代わりに分割規則 (splitting rule) を取り入れたものになっている。

DPLL アルゴリズムの流れ
1.単位節に含まれる変数に値を代入 (unit propagation)
　矛盾が起きたら探索打ち切り
2.適当なヒューリスティックで変数を選択
3.適当に選択した変数 (例えば a とする) に対し分割規則を適用し、
　a が真だった時と a が偽だった時の場合について、それぞれ再帰的に 2 分探索を行う
4.探索途中で、全ての論理式を満たす変数割当が見つかれば SAT
　全ての分岐で探索を行った結果、1 つも見つからなければ UNSAT

ここまで書いて思ったけどwikipedia見た方が早い予感…！