子句消去记数法分组定解算法

姜咏江

你想不到难题竟然这么简单！

有人认为子句消去记数法用到了对

2ⁿ个可能解标志的搜索，故而这就是指数型算法。虽然我一再强调2ⁿ个可能解标志只是一组数而已，但他们仍然认为n就是规模。其实，求解K-CNF-SAT的过程，将子句逐一消去的操作，显然与合取范式子句的数量有关。这个数量虽然有限制界，但具体合取范式子句多少，只与题目的具体设定有关。设合取范式k阶子句的数量为m，则去掉恒一子句，应有1≤m≤。这只是说决定动作的次数m的可能变化范围。在具体的K-CNF中，子句数量多少与n、k并无关系。

 

为了说明子句消去记数法并不以n为规模，我们采用可能解标识分组的方法来进行操作。这种分组只是在需要的时候会增加可能解标志的分组，不像穷举法那样2ⁿ个可能值需要一一验证，而是一次性得到全部解。

n个逻辑变量所有可能解可以用n个“*”表示（*本身表示0或1）。这样一来，最初的可能解标识我们就用*_n*_n-1*_n-2…*₂*₁一个字来表示（这里的下标只是说明位置，计算中不写）。我们在消去子句的过程中，将这个可能解标志进行分组，最后就能够求出合取范式满足的所有解。

1.              基本思想

根据子句消去记数法，消去一个非恒一子句，合取范式可能解标志集中，消去子句的变量位置至少会有一个是其反码表示的可能解标识留下。例如，消去子句x3+x5+x7’，那么10个变量的3-CNF的可能解标志组就变成了7个分组：

B=｛***0*0*0**，***0*0*1**，***0*1*0**，***1*0*0**，***1*0*1**，***1*1*0**，***1*1*1**｝。

集合B中*是0或1。

若再有子句x3’+x5’+x7，则恰有***1*0*0**被消去。则

B=｛***0*0*0**，***0*0*1**，***0*1*0**，***1*0*1**， ***1*1*0**，***1*1*1**｝

若有变量落在*的位置，则因*即可是0，亦可是1，所以可将本组分解。

例如，若再消去x3’+x5’+x10知从上次剩余标标志组B中知，该子句的标识落在***0*0*0**组中，被消去的为1**0*0*0**，将其消去，应剩0**0*0*0**。于是可能解变为：B=｛0**0*0*0**，***0*0*1**，***0*1*0**，***1*0*1**， ***1*1*0**，***1*1*1**｝；

若再有子句x3’+x7+x10’，但因该子句在标志组***1*1*0**中，消去这个子句，故B中***1*1*0**变为1**1*1*0**。

如此继续，直至全部子句消去，从剩下的用0、1和*表示的可能解标志取反，就可以得到全部解！

2.              子句消去记数法分组定解算法

子句消去记数法分组定解算法如下：

（0）       输入k阶合取范式；

（1）       设立一个n位字，每位都是“*”的可能解标志集B；

（2）       从头开始，逐一消去子句，恒一子句直接消去，若是非恒一子句，则依子句变量表达形式的采用拆分标志组，去掉相应标志组包含该子句的部分（若子句变量值正好与B的对应位相同，那么消去该组，不然从存在标志组中将其消去），获得剩余可能解标志组集合B；

（3）       重复（2），直至无子句或全部可能解标志组都被消去；

（4）       若B标志完全被消去，说明此合取范式无满足解，不然各可能解标识的0、1位分别取反码，*位分别选择0或1，得到的n位二进制数都是原合取范式的解。

为了能够具体了解子句消去记数法分组定解算法，我们用例子加依解释。

3.              算法例题

例题：5个逻辑变量的3阶合取范式

F=(x1’+x1+x3’)(x1’+x2’+x3’)(x2’+x3+x4)(x3+x4’+x5)(x1+x2+x3)(x2’+x4’+x5’) (x3’+x4’+x5’),

求满足F=1的解。

解：令B=｛*****｝，因(x1’+x1+x3’)是恒一子句，直接消去。

消去(x1’+x2’+x3’)，则剩余

B=｛**001，**010，**011，**100，**101，**110，**111｝；

再消去(x2’+x3+x4)，则因其标志在**100、**101中，消去*110*，剩，*0100，*0101，于是

B=｛**001，**010，**011，*0100，*0101，**110，**111｝；

再消去(x3+x4’+x5)，则因其标志在*0100、*0101、**110和**111中，则消去101**，剩00110、01110、11110、00111、01111、11111，于是

B=｛**001，**010，**011，00100，00101，00110，01110，11110，00111，01111，11111｝；

再消去(x1+x2+x3)，则因其标志在00111，01111，11111中，消去无剩余，得

B=｛**001，**010，**011，00100，00101，00110，01110，11110｝；

再消去(x2’+x4’+x5’)，则先消去00100和00101，则

B=｛**001，**010，**011，00110，01110，11110｝；

然后在标志**001，消去标志00001，剩余01001、10001、11001，则得

B=｛01001、10001、11001，**010，**011，00110，01110，11110｝；

再消去(x3’+x4’+x5’)，则在**010和**011中消去00010和00011，得

      B=｛01001、10001、11001，01010，10010，11010，01011，10011，11011，00110，01110，11110｝；  

根据标志取反得解方法，得此合取范式共有12个向量解，分别是B’＝｛10110，01110，00110，10101，01101，00101，10100，01100，00100，11001，10001，00001｝。

4.              子句消去记数法求解过程的多项式时间

对不起，多项式时间证明有修改，很快会登出。2015-8-11

 

5.              算法评价

子句消去记数法需要事先定义2ⁿ个可能解标识，会被误认为是算法的一部分。用子句消去记数法分组定解算法，无需先定义全体可能解标识，只是设置一个用*组成的n位表示字，在以后的子句逐步消去过程中分裂出一些分组，最后得到全部确定解的标识。在求解的过程中不增加不必要的可能解存储空间，也节省了消去那些不是解标识的操作步骤，因而会较子句消去记数法提高了速度，实际执行缩短了一定时间。

 

 

特别声明：此算法源自子句消去记数法，系本人独创，对用于商业市场行为保留追索发明权。

 

2015-7-27

 

 

 

 

 

转载本文请联系原作者获取授权，同时请注明本文来自姜咏江科学网博客。
链接地址：https://blog.sciencenet.cn/blog-340399-908661.html

上一篇：K-CNF-SAT人工子句消去计数法求解,兼答柳渝质疑
下一篇：k-CNF-SAT无解条件