CNF
連言標準形
Conjunctive normal form
連言標準形とは以下のように表現されるブール関数である
$ \Phi(\vec{v}) = \bigwedge_i \bigvee_j b_{i,j}$ b_{i,j} \in \{v_k, \neg v_k, ...\}
節(Clause)とは$ \bigvee_j \phi_{i,j}の部分
$ k-連言標準形, $ k-CNFとは全ての節の長さが$ kのCNFのことである
$ \Phi_k(\vec{v}) = \bigwedge_i \bigvee_{j \in k} b_{i,j}$ b_{i,j} \in \{v_k, \neg v_k, ...\}
任意のブール関数$ f : 2^l \to 2には同等の$ l変数のCNF$ \Phiが存在し、長さは$ O(l2^l) $ (\forall l)(\forall f : 2^l \to 2)(\exists \Phi : \text{CNF})[f = \Phi]
Proof.
$ |y|変数のCNF
$ \ne_{x}(y) := \bigvee_i n_{x_i}(y_i)
$ n_{0}(y_i) := y_i
$ n_{1}(y_i) := \neg y_i
$ x \ne y \iff n_{x}(y) = 1より$ x \ne y \iff \ne_{x}(y) = 1
CNFを次のように定義する
$ \Phi(v) := \bigwedge_{w:\ f(w)=0} \ne_{w} (v)
$ \Phi(v) = 0 \iff \exists w[f(w) = 0 \land \ne_{w}(v) = 0] \iff \exists w[f(w) = 0 \land w = v] \iff f(v) = 0 より$ f = \Phi
$ \ne_{x}(y)の長さは$ O(l)
よって$ \Phi(v)の長さは$ O(l \cdot 2^l) ❏