深入研究子句消去法

姜咏江

多项式C_n^k+C_n^k-1+...+C_n¹+C_n⁰与2ⁿ相差多少？其实，只要k=n，那么前者就是后者。只有当k为常数的时侯，多项式与指数时间复杂度才有明显的时间效益。

k为常整数，求由比k少的逻辑变量取值形成子句间与运算表达式结果为真值，就是SAT问题。如今SAT问题有了多项式时间复杂度的算法——子句消去法。但从多项式与2ⁿ之间的关系来看，当k很大的时侯，算法执行的复杂程度（或则说任务量）也会很大，这就需要我们去寻找子句消去法能更快执行的方法。这里先介绍一个减少判断变量可选解的方法。

子句消去法最坏的情况是从头到尾判断的每个变量都出现两个可选解。如果能够有方法减少判断变量的数量，自然可以加快计算。

选判定理：子句块无唯一解变量，其非关联变量都有2个可选解。

证明：依据二进制限位数性质，k阶子句块如果没有任何一个变量有2^k-1个表现值，那么至少有一对可以进入这个子句块的互反子句不在其中。由附件文中的定理2、3、4立即就可以得出此定理成立。

实际问题中的SAT问题，逻辑变量可能很多，而形成子句块共有的变量可能不多。在施行子句消去法求SAT解的过程中，先将各子句块中唯一解变量值确定，消去相关子句之后，剩下的都是无唯一解变量的子句块。此时只要去判断那些关联变量有几个可选解，就可以迅速地得出无解，或者求出SAT的满足解。

2016-11-12

附件：

子句消去法求k-SAT满足解（同行讨论稿）.pdf