nandaro

変数選択フェーズでは、現在の割り当てにおいて単位節が存在しない場合にある変数に真偽を適当に割り当てる。
様々なヒューリスティクスが存在するが、方法の良し悪しを判断する基準は以下のような感じ。

• 探索空間の枝刈りを目的に、素早く矛盾を引き起こす割当を行えること
• 全ての節の充足を目的に、出来るだけ多くの節を充足する割当を行えること

代表的な変数選択ヒューリスティクスを以下に挙げる。

• MOM (Maximum Occurrences on Minimum sized clauses)
• BOHM
• DLIS (Dynamic Largest Combined Sum)
• VSIDS (Variable State Independent Decaying Sum)

結論から言うと、一番最後に挙げた VSIDS が現時点では最も標準的なヒューリスティクスである。

以降は豆知識のようなもの。

MOM は現在で最小のサイズの節の中に最も多く出現するリテラルを選択する。
BOHM もサイズの小さい節に多く出現するリテラルを選択する。
DLIS は GRASP という 古い SAT ソルバで使われており、各リテラルの出現回数を記録するカウンタを用意する。
効果が高いこともあると言われているが、各リテラルを数えるコストやバックトラックの度にカウンタの再計算があるのが問題。