可满足性问题和消解法

命题公式的可满足性问题可归结为其 主合取范式 的可满足性问题.

不含有任何问题的简单析取式称为空简单析取式, 规定为不可满足的.

定义 设 $C_1,C_2$ 为两个简单析取式, 且 $C_1=l\vee C_1^{\prime },C_2=l^c\vee C_2^{\prime }$, 其中 $C_1^{\prime },C_2^{\prime }$ 不含 $l,l^c$, 则称 $C_1^{\prime }\vee C_2^{\prime }$ 为 $C_1,C_2$ 以 $l,l^c$ 为消解文字的消解式, 记为 $Res(C_1,C_2)$.

定理 $C_1\wedge C_2\approx Res(C_1,C_2)$.

$C_1\wedge C_2$ 与 $Res(C_1,C_2)$ 有相同的可满足性, 但是不一定等值.

消解序列

定义 设 $S$ 是一个合取范式, $C_1,...,C_n$ 是一个简单析取式序列, 如果对每一个 $i$, $C_i$ 是 $S$ 的一个简单析取式或是 $Res(C_j,C_k)$, 则称此序列是由 $S$ 导出 $C_n$ 的消解序列.

当 $C_n=\lambda$ 时, 称此序列是 $S$ 的一个否证.

指向原始笔记的链接