nandaro

1996 年に提唱された CDCL アルゴリズムによって、SAT ソルバは急速な成長を遂げたと言える。
CDCL とは Conflict-Driven Clause Learning の略で、このブログでは矛盾からの節の学習と非時間順バックトラックの 2 つを指すものとする。
(CDCLを組み込んだ DPLL アルゴリズムを CDCL と呼ぶ人も居る)

CDCL を DPLL に組み込んだソルバは CDCL ソルバと呼ばれており、
それが現在の SAT ソルバの実装の標準スタイルとなっている。

CDCL ソルバの動作を示す擬似コードを The Quest for Efficient Boolean Satisfiability Solvers から借りて、勝手にコメントを加えたものを載せる。

status = preprocess();                   //単位節の割当や、それに伴う伝播を予め行う
if(status!=UNKNOWN) return status;       //前処理の時点で結果が分かればそれを返す

while(1) {
　　decide next assignment();            //変数選択フェーズ
　　while(true) {
　　　　status = deduce();               //推論フェーズ
　　　　if(status == CONFLICT) {         //矛盾が起きた
　　　　　　blevel = analyze_conflict(); //衝突の解析＆学習フェーズ
　　　　　　if(blevel == 0)              //衝突を解析した結果、トップまで戻ってしまった(UNSAT)
　　　　　　　　return UNSATISFIABLE;
　　　　　　else backtrack(blevel);      //バックトラックフェーズ
　　　　} else if(status == SATISFIABLE)
　　　　　　return SATISFIABLE;
　　else break;                          //変数選択フェーズに戻る
　　}
}

コメントに載せたように、CDCL ソルバの解探索には4つのフェーズがあると言える。

• 変数選択フェーズ
• 推論フェーズ
• 衝突の解析＆学習フェーズ
• バックトラックフェーズ

CDCL の節の学習とか非時間順バックトラックって結局何なの？という説明はとりあえず置いておいて、これら4つのフェーズを次回以降の記事で触れていく。