神奇的子句消去法

姜咏江

连我自己都想不到子句消去法最终竟然如此简单神奇。这里给出100变量的3-SAT解题的例子。你可以选择任意的关联段求解，只要记住解题一般步骤如下：

1. 避免出现无解情况（找一个变量有4个相同值的子句块，为这个变量设定该值，消去相关子句）；
2.找出剩下的有唯一解动态子句块设定值，消去相关子句；
3. 继续2，直至全部剩余子句块都是多解；
4. 查找多解的剩余关联段可形成无解动态块，设值避免无解；

5. 独立的子句块单独求解；
6. 合成SAT的解。

如果最终出现多解动态块，可以用下面给定的方法记录：

两个变量的值是｛00、11｝，那么用33表示解为01和10；

两个变量的值是｛10、01｝，那么用22表示解为00和11；

两个变量的值是｛00｝，那么用vv表示解为0*和*0；

两个变量的值是｛11｝，那么用tt表示解为1*和*1；

两个变量的值是｛10｝，那么用kk表示解为1*和*0；

两个变量的值是｛01｝，那么用qq表示解为0*和*1；

*表示0或1。

注意：1至3的操作可以从局部进行，然后逐步扩充。如果某一个关联段无解，那么3SAT就无解。

您有兴趣可以试解此题，不会耗费多少时间。

练习例题：100个变量的3sat求解.xls

2015-11-26