姜咏江

消去块中唯一解，

不然找一可选解，

解多暂时一边放，

全多选解可得解。

《时间复杂度解释：

子句块变量唯一解的判断条件为有2^k-1个0或1，如果同时0和1都有2^k-1个SAT无解。

SAT的子句块最多有2^kC_n^k+2^k-1C_n^k-2+…+ C_n¹这多项式个，子句块变量最多为k个，k是一个常数，子句块可能重复的子句不会超过2^k-1C_n^k-2+…+ C_n¹个，所以对子句块去掉重复子句的操作不会超过一个常数，知时间复杂度总是O（1）。这样，对SAT全体子句块去重复子句的操作时间复杂度就是多项式O(n^k)。

可选解通过设定变量值，然后施行子句消去法，到关联剩余子句块全多解或关联段边界。

这一过程最多有可能进行2^kC_n^k+2^k-1C_n^k-2+…+ C_n¹个子句块消去操作，最坏每个变量操作2次，n个变量操作时间复杂度就是O(n^k+1)。

只要是变量全多可选解，那么可一次求出满足解。

这有定理保证。

结论：子句消去法时间复杂度不超过O(n^k+1)。

》

2016-11-8