融合原理の健全性と完全性

真偽値の変数 $x$ , およびその否定 $\overline{x}$ をリテラルという。リテラル, およびリテラルを論理和 $\lor$ で繋げた論理式を節という。さらに, 節, および節を論理積 $\land$ で繋げた論理式を節形式という。例えば,

$x_1$ , $\overline{x_2}$ はリテラル,
$x_1$ , $\overline{x_2}$ , $x_1 \lor \overline{x_2}$ は節,
$x_1$ , $\overline{x_2}$ , $x_1 \lor \overline{x_2}$ , $(x_1 \lor \overline{x_2}) \land (\overline{x_1} \lor x_3)$ は節形式。

変数 $\{x_1, \dots, x_k\}$ からなる節形式 $\phi$ があるとき, 写像 $\{ x_1, \dots, x_k \} \to \{0,1\}$ を $\phi$ の割当という。どんな割当についても真となる節形式 $\phi$ は恒真であるという。また, $\phi$ が真となるような割当が存在するとき, 節形式 $\phi$ は充足可能であるという。例えば,

節形式 $x_1 \lor \overline{x_1}$ は恒真である。
節形式 $(\overline{x_1} \lor \overline{x_3}) \land (\overline{x_1} \lor x_2 \lor x_3) \land (\overline{x_2} \lor x_3)$ は充足可能である。実際, $x_2 \mapsto 1$ , $x_3 \mapsto 1$ , $x_1 \mapsto 0$ という割当は $\phi$ を充足する。
しかし, 節形式 $(x_1 \lor \overline{x_2}) \land \overline{x_1} \land x_2$ は充足可能でない。後ろの二つのリテラルをいずれも真にするためには, $x_1 \mapsto 0$ , $x_2 \mapsto 1$ とする他ないが, すると $x_1 \lor \overline{x_2}$ が $0$ となってしまう故。このように充足可能でない, すなわち充足不可能な節形式が存在する。

ある節形式が充足可能かどうかを判定する問題を, 節形式の充足可能性問題 $\textit{CNF-SAT}$ という。これは理論と実用の両面から重要な問題として広く知られている。融合原理は, この問題を解くための論拠の一つとして知られる。

融合とは, 二つの節 $x \lor \cdots_{\,1}$ と $\overline{x} \lor \cdots_{\,2}$ から, 節 $\cdots_{\,1} \lor \cdots_{\,2}$ を作ることをいう。次の命題は明らか。

［命題1］節形式 $\phi$ の二つの節 $C = x \lor \cdots_{\,1}$ , $C' = \overline{x} \lor \cdots_{\,2}$ を融合して $\varphi = \cdots_{\,1} \lor \cdots_{\,2}$ を作ったとき, 同じ割当 $\sigma$ で $C \land C'$ と $\varphi$ を充足できる。すなわち,

$\forall \sigma$ . $\sigma$ が $C \land C'$ を充足する $\iff$ $\sigma$ が $\varphi$ を充足する.

いま, 節形式 $\phi = C_1 \land \dots \land C_m$ が与えられたとして, 次の手続き RES を繰り返す：

（１）節形式 $\phi$ から $C_i = x \lor \cdots_{\,i}$ と $C_j = \overline{x} \lor \cdots_{\,j}$ を選んで（ $i = j$ でもよい）, これらを融合し $C = \cdots_{\,i} \lor \cdots_{\,j}$ を作る。なお, 融合後の節 $C$ に重複するリテラルがあればひとつだけ残す。また,

$C \in \phi$ , もしくは
あるリテラル $x$ について $x$ と $\overline{x}$ のどちらも $C$ に含まれている

ならば融合失敗として, 融合を選び直す。どのように融合を選んでも失敗するなら文字列 "SAT" を出力して停止する。うまく融合を選べたら（２）へ。

（２）もし, 節 $C$ が空節 $\{\}$ ならば, 文字列 "UNSAT" を出力して停止する。そうでなければ, 節 $C$ を $\phi$ に加えた節を, 改めて $\phi$ と更新して（１）へ。

なお, この手続き RES は必ず停止する。なぜなら, この手続きは $\phi$ に $C \notin \phi$ となる新しい節 $C$ を加えていくが, この新しい節の種類は高々有限個しか存在しないからである。実際, 節形式 $\phi$ がもともと $k$ 種類の変数でできているなら, 節の種類はぜんぶで $\sum _ {r = 0} ^ {k} { _{k}\text{C}_{r} 2^r} (= 3^k)$ 個となって有限である。

この記事では, この手続き RES が $\textit{CNF-SAT}$ を決定すること, すなわち, 節形式 $\phi$ を入力とした RES の出力について,

（健全性） RES が "UNSAT" を出力するならば, $\phi$ は充足不可能であり,
（完全性） $\phi$ が充足不可能ならば, RES は "UNSAT" を出力する,

ことを証明する。

（証明）先の［命題1］から, RES における $\phi$ の更新前と更新後で充足同値が保たれる。すなわち, 更新前の $\phi$ が充足可能であることと, 更新後の $\phi$ が充足可能であることは同値である。したがって, RES が停止する直前の $\phi$ について主張を証明すれば, 入力の $\phi$ についても同じ主張がしたがう。

健全性のほうがたやすい。 RES が "UNSAT" を出力するということは, 空節 $\{\}$ が導かれたということになり, この空節を導いた節形式 $\phi$ の二つの節 $C_i, C_j$ が存在する。あるリテラル $x$ について $C_i = x$ , $C_j = \overline{x}$ としてよい。すると $\phi = \cdots \land x \land \cdots \land \overline{x} \land \cdots$ とかけるが, $x$ と $\overline{x}$ のどちらか一方は必ず偽だから, この $\phi$ は充足不可能である。

完全性については対偶を示す。すなわち, 次の主張：

RES が "SAT" を出力するならば, $\phi$ は充足可能である

を, $\phi$ に含まれる変数の種類 $k$ に関する帰納法で示す。

まず $k = 1$ として, この変数を $x$ とかけば, 論理的に $\phi$ は ① $x$ , ② $\overline{x}$ , ③ $x \land \overline{x}$ の三通りに限られる。①なら $x \mapsto 1$ , ②なら $x \mapsto 0$ とすれば $\phi$ を充足できる。そして③は起こり得ない；この $\phi$ からは空節を導けるので, RES が "SAT" を出力するという仮定に反するからである。よって, $\phi$ は充足可能である。

次に, RES が "SAT" を出力する直前の $\phi$ について, $\phi$ が $x_1, \dots, x_k$ からなる節形式ならば, $\phi$ の節の形は次の三通りに分けられる（ RES の定義から, $\phi$ の任意の節 $C$ について, $x$ と $\overline{x}$ の両方が同じ節 $C$ に現れる場合は除かれることに注意）：

$K_i^1 = x_1 \lor \varphi_{i}(x_2, \dots, x_k)$ ,
$K_j^2 = \overline{x_1} \lor \psi_{j}(x_2, \dots, x_k)$ ,
$K_l^3 = \xi_{l}(x_2, \dots, x_k)$ .

以下, $\phi$ を充足する割当 $\sigma$ を構成する。すなわち：

2の形が現れない場合。まず, 3の形の節 $K_l^3$ のみによる節形式 $\phi'$ を入力として RES を走らせると, 仮定からこの出力も "SAT" になるので(why?), 帰納法の仮定によってある割当 $\sigma'\mathpunct{:} \{x_2,\dots,x_k\} \to \{0,1\}$ が存在してこの $\phi'$ を充足する。したがって, $\sigma = \sigma' \lbrack 1 / x_1 \rbrack$ , すなわち $x_1 \mapsto 1$ , $x_r \mapsto \sigma'(x_r)$ $(r = 2, \dots, k)$ とすれば, $\sigma$ は $\phi$ を充足する。
1の形が現れない場合。上と同様にして示せる。
1と2の形がどちらも現れる場合。このとき, やはり上と同様に, 3の形の節のみからなる節形式 $\phi'$ を充足する割当 $\sigma'$ をとれば, この割当のもとで ① $\forall i. \varphi_{i} = 1$ または ② $\forall j. \psi_{j} = 1$ が成立つ；背理法によって示す。ある $i, j$ がとれて $\varphi_{i} = 0$ かつ $\psi_{j} = 0$ だったとすれば, $K_i^1$ と $K_j^2$ の融合である $K = \varphi_i \lor \psi_j$ も $0$ となる. しかるに $\sigma'$ の作り方から, この融合による節 $K$ が $\phi'$ に現れないことがわかる。ゆえに残る可能性はあるリテラル $x$ について $x$ と $\overline{x}$ がともに $K$ に含まれる場合, すなわち恒真である場合しかないが, これは $K$ が $0$ となったことに反する。よって, ① ならば $\sigma = \sigma'\lbrack 0/x_1\rbrack$ , ② ならば $\sigma = \sigma'\lbrack 1/x_1\rbrack$ とすれば, $\sigma$ は $\phi$ を充足する。

而して

ノートとかメモとか。

融合原理の健全性と完全性