sat-solvers - SAT ソルバー、深さ 0 の割り当て

Question

たとえばミニサットのような SAT ソルバーについて話すとき、「0-depth」と「CNF 割り当て」の値は何を意味しますか? これらの値は通常、さまざまな SAT ソルバーの情報出力の一部です。

Answer 1

深さゼロの代入は、DPLL 検索が開始される前に変数の値を設定しています。MiniSAT が行う数式の前処理 (包含、自己包含など) によって、変数が特定の値を持たなければならないことが証明される場合があります。可能であれば、MiniSAT は DPLL 手順を開始する前にそのような変数の値を修正します。