続き。同書では(変数)ないし¬(変数)を "literal"(リテラル) と呼び、literal のいくつかの論理和を "clause"(クローズ)と呼んでいる。clause のいくつかの論理積を CNF(Conjunctive Normal Form)と呼ぶ。全ての clause が k 個の literal からなるような CNF は k-CNF と呼ぶ。
例えば x[0] ∨ ¬x[2] ∨ x[3] のようなものは
boolean p = x[0] || !x[2] || x[3];
みたいに書ける。今夜はこの辺までにしておくか。
