乗法標準形
出典: フリー百科事典『ウィキペディア（Wikipedia）』
乗法標準形（英: Conjunctive normal form、CNF）とは、ブール論理における論理式の標準化（正規化）の一種であり、選言節の連言の形式で論理式を表す。主乗法標準形、連言標準形とも呼ぶ。正規形としては、自動定理証明で利用されている。
[編集] 概要
乗法標準形では、1つ以上のリテラルの論理和を1つ以上含む論理積の形式となる。加法標準形(DNF)と同様、CNF における演算子は論理積、論理和、否定だけである。
以下の論理式は CNF の一種である。
しかし、以下の論理式は CNF ではない。
上記の3つの論理式はそれぞれ下記の3つの乗法標準形の論理式と等価である。
リテラルは、変項（命題）か変項の否定であり、否定演算子はこの形でのみ出現する。全ての変項（またはその否定）を含む論理式を標準項と呼び、特に全ての変項（またはその否定）の論理和の形式になっている項を最大項と呼ぶ。従って、最大項の論理積の形式になっている論理式は、CNF である。この形式は、真理値表で出力が「偽」となる行を最大項として取り出したものを論理積で繋いだものであり、その真理値表に対応する論理式となっている。つまり、真理値表で表されるものは全て乗法標準形の論理式で表せ、組合せ回路も乗法標準形で表せる。
任意の論理式を CNF に変換するには、二重否定の除去、ド・モルガンの法則、分配法則といった論理的に等価な変換を行う法則を使う。全ての論理式は乗法標準形に変換できる。このため、証明に際して全ての論理式が CNF であることを前提とすることが多い。しかし、元の論理式によっては、CNF への変換によって論理式が極めて長大になることもある。例えば、次の論理式を CNF に変換すると、2n 個の項を書き連ねることになる。
等価性よりも充足可能性を満たすよう CNF に変換することで、論理式のサイズの指数関数的増加を招かない変換方式もある。このような変換方式でのサイズ増加は線形であることが保証されるが、新たな変項を導入する必要がある。
乗法標準形から節標準形を作ることができ、節標準形は導出に使われる。
計算複雑性理論における重要な問題の一種として、乗法標準形の論理式を「真」にする各変項の真偽の組合せを問う問題がある。これを充足可能性問題(SAT)という。変項が3種類の 3-SAT はNP完全問題（3変項以上のSATは全てNP完全）だが、2-SAT は多項式時間で解く事が出来る。
