子句消去法求任意SAT的满足解

姜咏江

SAT问题中可以有1到k个逻辑变量形成子句。如何用子句消去法求这样一般SAT的满足解？说起来方法十分简单，那就是先确定低阶子句的解，后确定高阶子句的解。

1.              举例说明

举例k=5。CNF如下：

CNF=x1(x’1+x2)(x’1+x’2+x5)(x’1+x’2+x’3+x4+x’5)(x’1+x’2+x’3+x’4+x’5)(x1+x’2+x’3+x’4+x’5) (x’1+x2+x’3+x’4+x’5) (x1+x2+x3+x4+x5)，求CNF=1的解。

操作顺序如表1至表4（绿色表示选择变量值后，欲消去的那些子句），最后求出SAT的满足解为：X1X2X3X4X5=110*1，其中“*”表示可以取值0或1。

表1  先选一阶子句

表2  后选2阶子句

表3  再选3阶子句

表4  最后选k阶子句

2.              总结

（1）       将变量正反都在同一个子句的子句全部消去，因为这样不改变SAT的满足解。

（2）       将低阶子句放到前面，高阶子句放到后面，按照先求低阶子句块和关联段的满足解，再求剩余高阶子句块和关联段满足解。

（3）       不论高低阶子句，求解中具有相同变量的变量值子句一律消去，最终n（n>=k）个变量值设定完成，无剩余子句，则所设值为SAT的解。

3.              子句消去法参考

http://blog.sciencenet.cn/blog-340399-947707.html

2016-1-10