姜咏江

子句消去法能够一次性求出k-SAT的满足解，基本思路十分简单。如果按照穷举法的思路，每一个逻辑变量都有0和1两个可能解值，因而n个变量组合到一起所成的k-SAT就要有2ⁿ个可能解，这样就会在最坏的情况下，要验证2ⁿ次才能够得到有解与无解的结果。

子句消去法的思路：假如k-SAT有解，那么每个变量的取值0或1，就都有可能使k-SAT有解或无解。能不能先确定哪些只能取唯一值变量？如果先将唯一值变量的相关子句都消去，那么剩下的子句就可以都是2个可选解了，即任选其中一个变量的0或1，再考察剩余的部分，进而可以得到剩余的SAT有满足解。

子句消去法的可选解是经过“唯一解”消去的判断方法确定的。这要用到我找到的子句块特有的结构规律，即用限位数理论确定的“k阶子句块中一个变量有2^k-1个相同表现值，不选这个值k-SAT就无解”。

判断变量有唯一解或有解也是通过子句消去法降阶操作完成的。方法是设定一个变量的0或1值，运用子句消去法逐步检查消去后得到的剩余子句块是唯一解、无解还是多解。如果是唯一解，就继续运用子句消去法，直至无解或多解。这样就可以认定设定的0或1是否是可选解。再去考察设定这个变量的另一个值。如果0和1都是其可选解就标记。然后去考查另外的变量。如果某个变量有唯一可选解，那么就可以实际运用子句消去法将k-SAT进行化简，对剩余的k-SAT继续这种方法，直到剩余的变量都有2个可选解。

当剩余的k-SAT每个变量都有2个可选解的时候，任选一个变量的一个值并施行唯一解消去法，就可以得到其关联段的一组解。不相关的另外的变量也施行此法，最终就可以得到所有变量使k-SAT成立的确定值。

    总结一句话：先选变量唯一解，变量全多可选解时，任意选一个值，仍然通过唯一解消去法确定其他变量值。

为了让有兴趣的网友能够真正理解子句消去法，并能够实际应用，附上论文和实际练习的简单例子。

2016子句消去法求k-SAT满足解.pdf

子句消去法求SAT满足解（例题）.pdf

全例题.xls

2016-10-18