CNF
連言標準形 Conjunction Normal Form
論理式において、変数もしくはその否定をリテラルという $ xも$ \lnot xもリテラル
1つ以上のリテラルの論理和の1つ以上の論理積の形で表される論理式のことを CNF という
$ \bigwedge_i\bigvee_jl_{i,j}
例えば$ (x_0\lor x_1\lor x_2)\land(\lnot x_2\lor x_3\lor x_4)
CNF の名前は論理学の用語でいうと選言節の連言の形式で表された論理式だから
証明の方法
元の bool 式の任意の部分式を CNF 形式に充足可能性保存変換をすることで、多項式時間帰着できることを示す 例
$ (a\land b)\lor c (ここからCNF の形ではない部分式$ (a\land b)をCNF式に変換したい)
$ (x\lor c)\land(x\Leftrightarrow a\land b) ($ a\land bの値を新たな変数$ xに写す)
$ (x\lor c)\land(x\lor \overline{(a\land b)})\land(\bar x\lor (a\land b)) ($ \LeftrightarrowをCNFの形に変換する)
$ (x\lor c)\land(x\lor\bar a\lor\bar b)\land(\bar x\lor a)\land(\bar x\lor b)
こんなふうに部分式を新たな変数をに写していく操作では変数も節も元の式の長さに対して多項式オーダーで増えていく
なので変換処理は多項式時間で終わる