連言標準形のソースを表示

'''連言標準形'''（れんげんひょうじゅんけい、''{{lang-en-short|Conjunctive normal form, CNF}}''）は、[[数理論理学]]において[[ブール論理]]における[[論理式 (数学)|論理式]]の標準化（正規化）の一種であり、[[選言]]節の[[連言]]の形式で論理式を表す。'''乗法標準形'''、'''主乗法標準形'''、'''和積標準形'''とも呼ぶ。正規形としては、[[自動定理証明]]で利用されている。

== 定義 ==
連言標準形とは <math>l_{i,j}</math> が[[リテラル]]の時、以下の形式をした論理式のこと。
:<math>\bigwedge_i \bigvee_j l_{i,j}</math>

内側の[[選言]]を'''節'''（{{lang-en-short|[[:w:Clause (logic)|clause]]}}）と呼ぶ。

== 概要 ==
連言標準形では、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>

'''[[リテラル]]'''（{{lang-en-short|[[:w:Literal (mathematical logic)|literal]]}}）は、変項（命題）か変項の[[否定]]であり、否定演算子はこの形でのみ出現する。全ての変項（またはその否定）を含む論理式を'''標準項'''と呼び、特に全ての変項（またはその否定）の[[論理和]]の形式になっている項を'''最大項'''と呼ぶ。従って、最大項の[[論理積]]の形式になっている論理式は、CNF である。この形式は、[[真理値表]]で出力が「偽」となる行を最大項として取り出したものを論理積で繋いだものであり、その真理値表に対応する論理式となっている。つまり、真理値表で表されるものは全て連言標準形の論理式で表せ、[[論理回路#組み合わせ回路|組合せ回路]]も連言標準形で表せる。

連言標準形から[[節標準形]]を作ることができ、節標準形は[[導出]]に使われる。

[[計算複雑性理論]]における重要な問題の一種として、連言標準形の論理式を「真」にする各変項の真偽の組合せを問う問題がある。これを[[充足可能性問題]](SAT)という。変項が3種類の 3-SAT は[[NP完全問題]]（3変項以上のSATは全てNP完全）だが、2-SAT は[[多項式時間]]で解く事が出来る。

連言標準形を論理式として見ると、充足可能性問題などの解法の一つとなる。左記の論理式の全ての充足解を求める手法として、[[二分決定図|二分決定グラフ]]で表現し、これを圧縮することで実用的に解を導くことができる場合がある<ref>Randal E. Bryant. "[https://www.cs.cmu.edu/~bryant/pubdir/ieeetc86.pdf Graph-Based Algorithms for Boolean Function Manipulation]". IEEE Transactions on Computers, C-35(8):677–691, 1986.</ref>。二分決定グラフには幾つかの種類があるが、充足可能性問題や最適化問題の解法として実用的に取り扱う手法が知られている。

== 連言標準形への変換 ==
任意の論理式は等価な CNF に変換することができる。これを行うには、[[二重否定の除去]]、[[ド・モルガンの法則]]、[[分配法則]]といった論理的に等価な変換を使う。全ての論理式は CNF に変換できるため、証明に際して全ての論理式が CNF であることを前提とすることが多い。しかし、元の論理式によっては、CNF への変換によって論理式が極めて長大になることもある。例えば、論理式

:<math>(X_1 \wedge Y_1) \vee (X_2 \wedge Y_2) \vee \dots \vee (X_n \wedge Y_n)</math>

を CNF に変換すると、<math>2^n</math> 個の節を書き連ねることになる。実際、対応する CNF は

:<math>(X_1 \vee X_2 \vee \cdots \vee X_n) \wedge (Y_1 \vee X_2 \vee \cdots \vee X_n) \wedge (X_1 \vee Y_2 \vee \cdots \vee X_n) \wedge (Y_1 \vee Y_2 \vee \cdots \vee X_n) \wedge \cdots \wedge (Y_1 \vee Y_2 \vee \cdots \vee Y_n)</math>

となる。この式は <math>2^n</math> 個の節があり、それぞれの節は各 <math>i</math> について <math>X_i</math> または <math>Y_i</math> を含んでいる。

等価性よりも[[充足可能性問題|充足可能性]]を満たすよう CNF に変換することで、論理式のサイズの指数関数的増加を招かない変換方式もある。このような変換方式でのサイズ増加は線形であることが保証されるが、新たな変数を導入する必要がある。たとえば、上の論理式は新たな変数 <math>Z_1,\ldots,Z_n</math> を導入することにより CNF

:<math>(Z_1 \vee \cdots \vee Z_n) \wedge
(\neg Z_1 \vee X_1) \wedge (\neg Z_1 \vee Y_1) \wedge
\cdots \wedge 
(\neg Z_n \vee X_n) \wedge (\neg Z_n \vee Y_n) </math>

に変換できる。この論理式は新たな変数の少なくとも 1 つが真のときにのみ成立する。<math>Z_i</math> が真のとき、<math>X_i</math> と <math>Y_i</math> の両方が真であり、<math>Z_i \equiv X_i \wedge Y_i</math> を新たな変数として導入したことに相当する。この論理式が満たされるとき、元の論理式も同時に満たされる。その一方で、<math>Z_i</math> は元の論理式では使用されていないので、各 <math>Z_i</math> の値は元の論理式の値とは無関係であり、変換後の論理式においてはそうではない。つまり元の論理式と変換後の論理式は、充足可能性においては等価 ([[:en:Equisatisfiability|英: equisatisfiable]]) であるが、論理的に等価 ([[:en:Logical equivalence|英: equivalent]]) ではない。

== 脚注 ==
{{脚注ヘルプ}}
{{Reflist}}

==関連項目==
* [[選言標準形]]
* [[ブール関数#リード・マラー標準形|リード・マラー標準形]]
* [[ホーン節]]
* [[クワイン・マクラスキー法]]

{{logic}}

{{DEFAULTSORT:れんけんひようしゆんけい}}
[[Category:標準形 (論理)]]
[[Category:数理論理学]]
[[Category:数学に関する記事]]