子句消去法如何避免进入无解分支求解

姜咏江

合取范式3-CNF=1的解是由n个逻辑变量的可满足取值所决定的，用子句消去法求解时，只要一个逻辑变量无法确定使子句值为1，那么整个3-CNF=1就无解。实际上，整体的3-CNF=1是由一些局部的性质所决定的。这种局部特征集中体现在子句块和关联段，并且随着变量值的设定子句块和关联段都在缩小，特别是关联段，随着子句的消去，会划分成更小的关联段。因而用子句消去法求解3-CNF=1，常常是分为一些局部求解。在求解中只要我们记牢无解的基本结构，就可以避免进入无解的情况，从而顺利地逐步获得满足解。

1.             合取范式3-CNF=1无解的基本结构

用子句消去法求3-CNF=1的解，先要清楚无解的情况。一般来说，3-CNF=1只有三种结构会出现无解。

（1）子句块有8个子句；

（2）有两个变量的值已经确定，无法设定第三个变量的值；

（3）有一个变量的值已经确定，其余两个变量表示的子句有4种不同基本类型。

2.             唯一解值类型

子句块中变量写出的0或1称为变量表示值，而消去子句选择的0或1称为变量的解值。变量解值一经选定，该变量表示值与之相同的子句都可以消去。如果一些子句能够被唯一的一组解值消去，则称该组值为唯一解值。

局部的唯一解是求解3-CNF=1的关键，熟练掌握唯一解的情况，就能够快速地得到整体解。

3-CNF=1唯一解值类型如下：

（1）子句块有一个变量有4个一样的表示值。

因为一个子句块若有一个变量有4个相同表示值，那么其余两个变量的表示值一定形成了00，10，01，11这四种，不然就出现了重复数。此时只有选择那一个有4个相同表示值做为该变量解值，那么才不会出现无解。

（2）子句块两个变量值确定，第三个变量只有一种表示值。

（3）子句块有3个子句，且一个变量值已经确定。

这种情况待选值变量取值以表示值多的为准。例如子句块中x₁已经确定为0，有子句块如下：

x₁  x₂   x₃

1  0   0

1   1   0

1  0   1

这时只要设定x₂=0， x₃=0即可。

3.             关联段求解顺序

懂得了无解和唯一解的结构，按照下面的操作顺序，3-CNF=1求解就不是难事。

（1）先检查是否有8个子句的子句块，没有转（2）。

（2）找子句块有4相同表示值变量，设定该值，消去相应子句，否则转（3）。

（3）都是多解子句块，找出关联子句块设定一个块解，消去相应子句，转（4），若出现无解，则结束。

（4）对剩余子句块先求唯一解，后定多解，直至关联段结束或多解转（3）。

4.             几点说明

（1）子句消去法求解合取范式满足解的方法具有很强的鲁棒性。即使整个3-CNF=1无解，我们仍然可以确定出有解的部分和无解的部分，这对做多因素分析十分重要。

（2）如果我们在实际问题研究中归纳出了k-CNF-SAT，那么你可以将k-CNF-SAT归约成3-CNF-SAT获得一些满足解（参考：http://blog.sciencenet.cn/blog-340399-945744.html）。

（3）运用表上作业的子句消去法求3-CNF=1的解，是一个对n个变量设值的过程。这种设值过程不需要重复，只要进行n次即可，因而子句消去法完全是一种O(n)的多项式时间复杂度的算法。不妨随便写出一个3-SAT，用子句消去法求解试试，速度之快，超出以往的想象。

 

2015-12-25

 

 

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

上一篇：柳渝你还认为子句消去法证明的是P=P吗？
下一篇：3SAT多关联段求解训练例题