详细解答3CNF求解运算器

姜咏江

为了介绍我的子句消去计数法（见http://blog.sciencenet.cn/blog-340399-905817.html）如何能够快速求出k-CNF-SAT的全部解，我在博文《3－CNF一秒钟求出解》中给出了求解运算器时序仿真截图。这张图包括P/NP专业人士也多有不解之处，提出了多长时间能够得出结果的疑问。为了能够解释诸多疑惑，我有必要对求解运算器时序仿真图进行详细一点的解释，并增加一个求解实例，通过实例说明子句消去计数法是一个快速解题算法。

例1，求下面合取范式的满足解。

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

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

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

该运算器求解结果如下图1，懂得了我的子句消去计数法，你立即就可以看出解是多少了。

图1  具有唯一解

为了能够让您迅速看懂这张仿真图，我先要介绍一下图中各部分的意义。

最左侧一栏是输入输出标志栏，箭头中的i或o分别表示输入子句或输出标识。

Name一栏是可选的非恒一子句，由于软件中不允许撇号做名称符号，故而将非运算符用下划线替代。例如“_x2_x3x5”表示的是x2’x3’x5。

再右面的一大宽栏是输入输出栏。上面横向有以纳秒为单位的计时，图1中仿真的时间在30纳秒到110纳秒之间。

逻辑变量值为0，用下细实线表示，值为1，用上实线表示。如果是逻辑向量，可以直接用多位二进制数表示。变量c是32位的向量，故用32位二进制数表示。

可能有的专家已经发现，所谓一侧计数器的名称正好与全体二进制限位数（一定位数的用数码0或1占位写出的数）一一对应。而在子句消去记数法中，有解存在，正好是那些值为0的计数器名称的反码。这样求解的过程中，只要找到值为0的计数器，就可以得到合取范式的解了！

为此，我设计了每个一侧计数器为1标识（当然也可以设计成为0标识），并将全体为1标识组成一个向量。图1中最下面的输出变量c是32个一侧计数器的非零标志线组成的向量，从右到左，分别表示一侧计数器0号至31号不为0标志。如果某位置是1，即表示该位置编号的计数器不为零；如果为0的，就表示该计数器的值是0。

例1给出的合取范式用子句消去计数法，进行求解，只有2号计数器值仍然是0。2号计数器的名称是x5'x4'x3'x2x1'，于是依子句消去计数法，此合取范式有惟一解x5=1,x4=1,x3=1,x2=0,x1=1。

子句消去计数法运算器用多长时间可以求出合取范式满足解？

从图1我们可以看到只要通过器件的20纳秒延时之后，就可以得到合取范式的解，也就是在我使用的微电子设计器件中，不超过30纳秒就可以得到全部解了！

为增加感性认识我们再给一个例子及截图，看看如何一次性求出全部解。

例2，有合取范式如下，求出全部解。

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

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

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

图2  多解截图

有解：x5=1,x4=1,x3=1,x2=0,x1=1

第11号计数器值为0，名称是x5’x4x3’x2x1，故有解x5=1,x4=0,x3=1,x2=0,x1=0

第27号计数器值为0，名称是x5x4x3’x2x1，故有解x5=0,x4=0,x3=1,x2=0,x1=0

第31号计数器值为0，名称是x5x4x3x2x1，故有解x5=0,x4=0,x3=0,x2=0,x1=0

我们可以验证，这四组值都是例2合取范式的满足解。

 特别声名：合取范式运算器是本人独创，一切用本方法设计合取范式运算器形成的市场行为，必须经本人同意。

2015-7-23

转：http://blog.sciencenet.cn/blog-340399-928224.html