100个变量的3-SAT求解实例

姜咏江

用分关联段子句消去法求3-SAT的满足解并不困难。我这里有一个100个变量的求解实例。手工操作也用不了多长时间。求解时，要先找有唯一解的子句块，从各个唯一解的子句块解出发，运用剩余动态块有唯一解的判定，做起来并不困难。遇到段多解留在最后处理，可以按需要取值。如果将多解留下，最终可以表达出更多的解。第二张表就是这个意思。

我用Excel的窗口分割，将解的变量值设定放在上面，滚动下面窗口，不影响观查变量直的设定。为了朋友们能够观看过程，仍然用绿色覆盖消去的子句，其实直接消去操作起来更容易。

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

 100个变量的3sat求解.xls

2015-10-8