連言標準形 (CNF - Conjunctive Normal Form)

連言標準形（CNF）は、節の論理積として書かれ、各節がリテラルの論理和になっている形式である。SATソルバー、制約処理、反駁に適した表現になる。

仕組みと確認

式を節へ分解し、各節のリテラルと変数の意味を記録する。変換後の式が元と同値か、補助変数を使う場合は少なくとも充足可能性を保つかを確認する。

限界と注意点

CNF化で式のサイズが急増することがある。空節・空節集合、重複リテラル、単位節、入力仕様の誤ったエンコードを境界例としてテストする。