姜咏江

SAT的定义中是不允许出现重复子句的，但在子句消去的过程中，会出现降阶的子句块中有重复的子句。t阶子句块变量唯一解是因为它有2^t-1个相同的表现值（1≤t≤k）。在消去子句的过程中很难事前知道那些子句会重复，这样证明消去重复子句这一步算法时间复杂度为多项式时间就很困难。不过我们可以从总体上来探讨。

假如SAT子句的最高阶是k，那么子句块的总数不会超过C_n^k+C_n^k-1+...+ C_n¹个。如此有m个变量表现值相同的子句块（1≤m≤k-1）最多有C_n-m^k-m+C_n-m^k-m-1+...+ C_n-m¹+1个，那么有m个变量表现值相同的子句块的子句总数不会超过C=2^k-m+2^k-m-1+ ...+1 个。C是一个有限常数。因此，任何一个剩余的子句块的子句数数，都不会超过这个数。在小于常数C个数中，消去重复数的算法时间复杂度无疑是O(1)。而剩余子句块最多还是C_n^k+C_n^k-1+...+ C_n¹个，所以SAT总体去掉子句块中重复子句的算法时间复杂度是O(n^k)。

2016-11-9