連言標準形
連言標準形（れんげんひょうじゅんけい、英: Conjunctive normal form, CNF）は、数理論理学においてブール論理における論理式の標準化（正規化）の一種であり、選言節の連言の形式で論理式を表す。乗法標準形、主乗法標準形、和積標準形とも呼ぶ。正規形としては、自動定理証明で利用されている。
定義
連言標準形とは [math]l_{i,j}[/math] がリテラルの時、以下の形式をした論理式のこと。
- [math]\bigwedge_i \bigvee_j l_{i,j}[/math]
概要
連言標準形では、1つ以上のリテラルの論理和を1つ以上含む論理積の形式となる。選言標準形(DNF)と同様、CNF における演算子は論理積、論理和、否定だけである。
以下の論理式は CNF の一種である。
- [math]A \wedge B[/math]
- [math]\neg A \wedge (B \vee C)[/math]
- [math](A \vee B) \wedge (\neg B \vee C \vee \neg D) \wedge (D \vee \neg E)[/math]
- [math](\neg B \vee C).[/math]
しかし、以下の論理式は CNF ではない。
- [math]\neg (B \vee C)[/math]
- [math](A \wedge B) \vee C[/math]
- [math]A \wedge (B \vee (D \wedge E)).[/math]
上記の3つの論理式はそれぞれ下記の3つの連言標準形の論理式と等価である。
- [math]\neg B \wedge \neg C[/math]
- [math](A \vee C) \wedge (B \vee C)[/math]
- [math]A \wedge (B \vee D) \wedge (B \vee E).[/math]
リテラル（英: literal）は、変項（命題）か変項の否定であり、否定演算子はこの形でのみ出現する。全ての変項（またはその否定）を含む論理式を標準項と呼び、特に全ての変項（またはその否定）の論理和の形式になっている項を最大項と呼ぶ。従って、最大項の論理積の形式になっている論理式は、CNF である。この形式は、真理値表で出力が「偽」となる行を最大項として取り出したものを論理積で繋いだものであり、その真理値表に対応する論理式となっている。つまり、真理値表で表されるものは全て連言標準形の論理式で表せ、組合せ回路も連言標準形で表せる。
任意の論理式を CNF に変換するには、二重否定の除去、ド・モルガンの法則、分配法則といった論理的に等価な変換を行う法則を使う。全ての論理式は連言標準形に変換できる。このため、証明に際して全ての論理式が CNF であることを前提とすることが多い。しかし、元の論理式によっては、CNF への変換によって論理式が極めて長大になることもある。例えば、次の論理式を CNF に変換すると、2n 個の項を書き連ねることになる。
- [math](X_1 \wedge Y_1) \vee (X_2 \wedge Y_2) \vee \dots \vee (X_n \wedge Y_n).[/math]
等価性よりも充足可能性を満たすよう CNF に変換することで、論理式のサイズの指数関数的増加を招かない変換方式もある。このような変換方式でのサイズ増加は線形であることが保証されるが、新たな変項を導入する必要がある。
連言標準形から節標準形を作ることができ、節標準形は導出に使われる。
計算複雑性理論における重要な問題の一種として、連言標準形の論理式を「真」にする各変項の真偽の組合せを問う問題がある。これを充足可能性問題(SAT)という。変項が3種類の 3-SAT はNP完全問題（3変項以上のSATは全てNP完全）だが、2-SAT は多項式時間で解く事が出来る。
連言標準形を論理式として見ると、充足可能性問題などの解法の一つとなる。左記の論理式の全ての充足解を求める手法として、二分決定グラフで表現し、これを圧縮することで実用的に解を導くことができる場合がある[1]。二分決定グラフには幾つかの種類があるが、充足可能性問題や最適化問題の解法として実用的に取り扱う手法が知られている。
脚注
- ↑ Randal E. Bryant. "Graph-Based Algorithms for Boolean Function Manipulation". IEEE Transactions on Computers, C-35(8):677–691, 1986.