連言標準形 (CNF - Conjunctive Normal Form) ・主乗法標準形 (Maxterm Expansion)

連言標準形（CNF）と主乗法標準形（maxterm expansion）は、論理式を節の論理積で表す関係にある。一般のCNFが任意の節を許すのに対し、主標準形では真理値表で式が偽になる各行から最大項を作り、構造を揃えて表現する。

仕組みと確認

真になる行と偽になる行を取り違えず、各maxtermが対応する割り当てで偽になることを確認する。一般CNF、主標準形、補助変数を用いたSAT向け変換を区別し、元の式との同値を真理値表で検査する。

主標準形は説明には明快だが、変数数に対して項数が急増する。ソルバー利用では、等価性を保つ必要があるのか充足可能性だけでよいのかを明示し、入力の未使用変数も確認する。