姜咏江

逻辑变量的可满足性问题SAT的破解，用子句消去法求解需要解决五个层面的问题。

第一，k阶子句块什么情况下无解？

k阶子句块有2^k个不同的子句，则一定无解。例如，3个变量的子句块如果有8个不同的子句，那么合取范式CNF=1一定无解。改变一下判断方法：一个变量在k阶子句块中有2^k-1个0和1，那么CNF=1一定无解。

第二，什么情况下变量在子句块中有唯一解？

在k阶子句块中变量只有2^k-1个0或1（不同时有）。例如，三个变量的子句块中某变量有4个0，那么这个变量必须取值0。

第三，不同子句块中的同一个变量什么情况下无解？

这就是变量在不同子句块中都有唯一值，但出现了矛盾。即一个值是0，同时在另一个子句块中必须是1，这时合取范式CNF=1无解。

第四，变量的值不是0就是1，可以选择哪个？

变量在子句块中虽然可以取值0或1，但由于子句块间的关联关系，变量取值要受到制约。子句消去过程中不产生矛盾的变量值叫变量可选解。可选解有一个的变量就是关联变量的唯一解。有两个可选解的变量取值，放到最后每个变量都有两个可选解的情况处理。

第五，每个变量都有两个可选解，如何选择变量值？

这种情况下合取范式CNF=1一定有解，但选择值时要避免出现矛盾。因为当前面的变量已经取定0或1的时侯，后面的变量要选择0或1，就要满足前面变量取值的交叉关系，不能出现矛盾选择（有定理保证存在不矛盾取值）。

子句消去法的基本思想是：先将必然选择值的变量确定后，消去相关子句，然后处理可以任意取值的变量，但要避免选择的矛盾。

如果以上五个层面的问题都在消去子句的过程中处理好了，那么任何合取范式的求解都不在话下。

SAT问题最复杂的情况是每个变量都有两个可选解。这时必须将它们的可选解值列表，当要每次选择变量值时，查表依据前面选定值来确定这个变量的值。

由于SAT的二进制数表示的子句总数不超过2C_n¹+2²C_n²+2³ C_n³+...+2^(k-1) C_n^k-1+2^k C_n^k，k是常数，这就是一个k次多项式，子句消去法以子句为处理的基本单位，因而子句消去法算法的时间复杂度不会超过O(n^k+1)。

k是小于n的常量。上面这个多项式与2ⁿ相比，只有当n大到一定程度，才会体现出多项式算法的“快速”性。如果k很大，仍然会感到“很慢”，但由于合取范式CNF有很多特别情况，研究这些特别情况，可以得到比DPLL算法快得多的算法。

2017-2-6