3-SAT分段子句消去法求唯一解例题

姜咏江

利用子句块唯一解和动态块唯一解来处理3-SAT求解，最方便的是3-CNF=1有唯一解的情况。这也是用其他方法求解3-SAT问题最不易的事情。

在用关联段子句消去的过程中，如果出现动态块消去呈现多解的情况，如果选择的变量值不合适，有可能出现后续无解的情况。正确的做法是暂不设值，而是沿着一元关联的子句块寻找唯一解的剩余子句块。只要找到关联的满足唯一解的子句块，就可以先设定这个子句块的变量值，然后反方向去确定前面多解的选值，这样可以最终正确地求出3-SAT的解。如果最终都是多解的子句块，那么这个3-SAT的问题肯定是多解了，此时确定最后一个子句块解，反向可得解。

3-SAT有唯一解的情况，用分段子句消去法既方便又准确。有兴趣的朋友不妨试试。我还没有编写程序处理。不过手工操作弄个百八十个变量也不是难事。就是上千个变量也未必是难事，操作过程中随着子句的消去，工作量会迅速减少，时间自然会加速减少。

本文给朋友一个唯一解的例子，希望有心人能够自己做做看，体会一下求解3-SAT问题的关键点在何处。表下面一行是实际消去子句后的结果。

唯一解实例：3-SAT分段子句消去法唯一解例题.xls

参考：http://blog.sciencenet.cn/blog-340399-925143.html

2015-10-6