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