nandaro

推論フェーズでは、変数選択を基に連鎖的に値を決定できる変数を探し真理値を割り当てる。
これもまた、色々な手法が提案されている。

• Unit Literal Rule (Unit Clause Rule)
• Pure Literal Rule
• Equivalence Reasoning
• Subsequent Research
etc...

色々書いといてなんだけど、一番上の Unit Literale Rule 以外は全て忘れよう。

Unit Literal Rule とはその名の通り、未定リテラルを 1 つしか持たない節 (Unit Clause, 単位節) があったら
その節が含むリテラルを true にするような割当を行う規則。
これを繰り返す仕組みを BCP (Boolean Constraint Propagation, 単位伝播) と呼ぶ。
推論といえば BCP を連想して良いくらいに皆 BCP を利用している。
そして実は BCP には色々な実装手法があるので一応列挙しよう。

• 監視リテラル方式
• カウンタ方式
• Head/Tail List方式

昨今では監視リテラル方式が主流。一番上以外は忘れよう(適当)。