k-CNF-SAT消去法求解

姜咏江

   用真值表的操作完全可以解决求解n-CNF-SAT问题。由于合取范式的变量具有交换律，故而在真值表中将变量按序确定取值并不失一般性。欲求合取范式f(x₁,..., x_n)=1的解，则每个子句值必须为1。这样可用设定值方式，不断消去为1的子句，最后求得函数f(x₁,..., x_n)=1的一些解。

   我们通过例子来说明逐步消去法求解的方法。

例子：设f(x₁,..., x₆)= (x1+x1'+x2')(x2+x3+x4)(x1'+x3'+x4')(x1'+x2+x5')(x2+x3+x6)(x1+x5+x6')，求满足f(x₁,..., x₆)=1的解。

该例子有多种解法。 可先消去恒为1子句，然后按以下方法求解。

解1：

（1）令x1＝1，消去为值为1的子句，剩(x2+x3+x4)(x1'+x3'+x4')(x1'+x2+x5')(x2+x3+x6)；

（2）令x2＝1，消去为值为1的子句，剩(x1'+x3'+x4')；

（3）令x3=0或x4=0，则无有剩余子句，于是得解（110***）或（11*0**）

注：*表示为0或1。

解2：

（1）令x1＝0剩(x2+x3+x4) (x2+x3+x6)(x1+x5+x6')；

（2）令x2＝1剩(x1+x5+x6')；

（3）令x5＝1或x6=0，其余任意。得解（01**1*）或（01***0）。

显然，从x₁到x_n每个变量都可以这样取0和1来求值。

逐步消去法到无子句时结束。

2.              讨论

（1）    由于每一逻辑变量可以取值0或1，故  f(x₁,..., x_n)的n个变量的值向量最多可有2ⁿ个。

（2）       f(x₁,..., x_n)=1的求解过程，只要前确定值使某子句值为0，则断定前面值向量组成的n元向量不是解。

（3）       f(x₁,..., x_n)值为1和为0是否各有一半？

（4）   解结果对错可以验证。

（5）  k-CNF-SAT子句最多有C_2n^k个。

(君子所为：个人研究心得，引用请注明出处)

2015-06-29