K-CNF-SAT人工子句消去计数法求解

姜咏江

N元变量的k个变量或其非组成的合取范式k-CNF的可能解有2^N个。依据子句消去记数法，只要消去子句的过程中有一个可能解的反码不为0，那么这个可能解就被排除了。如此我们可以设定2^N个标志位，令其初值为0。当消去子句的变量按照自身为1，反表示为0的原则，去掉可能解中对应位相同的标志，这样一次最多可排除2^N-k个可能解。这样最多经过次，可以确定k-CNF的全部解或无解。

1.              设计解标志

例如，5个变量组成的3阶合取范式的可能解为

00000 00001 00010 00011 00100

00101 00110 00111 01000 01001

01010 01011 01100 01101 01110

01111 10000 10001 10010 10011

10100 10101 10110 10111 11000

11001 11010 11011 11100 11101

11110 11111

可以将1用变量表示，0用变量非（带下划线）表示，得到解标志：

x5x4x3x2x1 , x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1。

2.              消去子句与可能解标志

随便找到一个不含恒一子句的3阶合取范式为例：

(x1’+x2’+x3’)(x3+x4+x5’)(x2+x4’+x5)(x1’+x2’+x3)(x2’+x3’+x4)(x1’+x4’+x5)

第一个子句是(x1’+x2’+x3’)，那么在解标志中找到有x3x2x1的标志消去子句和这些标志，得剩余合取范式：

(x3+x4+x5’)(x2+x4’+x5)(x1’+x2’+x3)(x2’+x3’+x4)(x1’+x4’+x5)

得可能解剩余标志：

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1。

第二次，消去子句(x3+x4+x5’)和含有x3x4x5的解标志，得

剩余合取范式：(x2+x4’+x5)(x1’+x2’+x3)(x2’+x3’+x4)(x1’+x4’+x5)

解标志：

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1。

第三次，消去子句(x2+x4’+x5)和含有x3x4x5的解标志，得

剩余合取范式：(x1’+x2’+x3)(x2’+x3’+x4)(x1’+x4’+x5)

解标志：

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1,  

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1。

第四次，消去子句(x1’+x2’+x3)和含有x1x2x3的解标志，得

剩余合取范式： (x2’+x3’+x4)(x1’+x4’+x5)

解标志：

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1,

x5x4x3x2x1,  

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1。

第五次，消去子句(x2’+x3’+x4)和含有x2x3x4的解标志，得

剩余合取范式： (x1’+x4’+x5)

解标志：

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1,

x5x4x3x2x1,  

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1。

第六次，消去子句(x1’+x4’+x5)和含有x1x4x5的解标志，得

没有了剩余合取范式。剩余解标志为：

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1,

x5x4x3x2x1,  

x5x4x3x2x1, x5x4x3x2x1, x5x4x3x2x1,

x5x4x3x2x1, x5x4x3x2x1。

3.              如何确定所有解

通过子句的消去来消去那些不可能满足合取范式的解标志，总以一方没有剩余而结束。但消去的过程都是依据存在的子句进行的，而不是依据可能解标志一方。如果在操作的过程中，可能解标志集被清空，则最初的合取范式一定没有满足解。

本例的可能解标志剩余很多，这些剩余解标志的反码都是最初合取范式的解。例如有标志x5x4x3x2x1,那么有解00010，即x1=0,x2=1,x3=0x4=0x5=0是所求解。

其他的解立即可以通过解标志取反都得到。

4.              可以更简单一些

如果你是一个熟悉从真值表如何抽象逻辑表达式的人，那么不用再去构造什么可能解标志了，而只要知道有多少个变量，就可以知道所谓的解标志，不过是一定位数的二进制数而已。例如已知n=6，那么解标志集就是000000到11111的2⁶＝64个无效0要写的限位数而已。这个2ⁿ个可能解标志集对任何的k≤n都适用。消去时，只要将xi的表示去找n位数对应的第i位是1，xi’对应的第i位是0，就能把该消去的解标志消去了。

5.              解题时间的问题

子句消去记数法中不论何时，合取范式和可能解标志集都是已知的。因而不能够将合取范式的构造和可解标志集列入算法时间。

对于合取范式满足求解，可以通过穷举法进行，这无疑要将2ⁿ个n位二进制数全部验证一遍，因而重复操作的次数是2ⁿ。

对于子句消去记数法，我们不难看到，子句消去计数法的执行操作次数仅仅依据给出的合取范式。由于去掉恒一子句后，子句最多有个，因而子句消去记数法的操作最多是次。子句消去记数法会因为给出的子句数减少，而明显地减少操作次数，这一点穷举法是做不到的。显然子句消去记数法操作过程耗费的是所谓的多项式时间，这与可能解标志的数量多少无关。

是一个典型的多项式表达式，此表达式的值很可能有>2ⁿ，但从所谓的算法多项式时间来看，依据来进行操作，就是多项式时间复杂度，而依据2ⁿ来操作就是指数型时间复杂度，这中间的关节我们暂时不去研究。但就那所谓的传统的、被人们认可了的“多项式时间复杂度”来说，子句消去记数法的操作无疑是多项式时间。

2015-7-25