3SAT解题步骤与规则

姜咏江

随着我对3SAT的分段子句消去法的深入，使求解3SAT的过程也在不断地瘦身，此次介绍的分段子句消去法步骤更加简单化，解法更加易学。

一、规则

运用分段子句消去法求解3SAT的满足解，要遵循如下两条规则：

（1）处理好可能无解子句块。

3SAT数值表示法可能无解的子句块只有一种。那就是有4个同值变量的子句块。例如下表1中x1x3x4的子句块有4个子句的x1值是0。此种情况必需设定x1=0，不然会进入无解状态。

表1

（2）多值可选应避开无解的动态块。

有2个变量需要共同确定值的二元关联子句块间选值不当，可能出现无解状态。例如下表2中关联的两个子句块都有多解，如果先选择了x1＝1和x5＝0，那么将会出现无解的动态块。而改变选值就会得到有解的情况。

表2

不论（1）或（2）都出现了将要确定变量的值无法选择的情况，即不论选择0还是1都无法将子句全部消去。

以上求解3SAT的规则都可以从【1】的定理8直接得到。

二、步骤

对没有8个子句的子句块组成的数值表3SAT，进行如下步骤的操作可以求出满足解。

（1）将所有子句块中一个变量有4个相同值的变量设定其值，消去相应子句；

（2）确定剩余子句中有唯一解的动态子句块解，并消去相应子句；

有唯一解的动态子句块特征有二：一是两变量值已经确定，第三个子句相同变量值都一样；二是一个变量值已经确定，其余子句相同二变量只能组成3种2SAT子句（如果组成4种2SAT子句则无解）。

（3）最后设定所有多解的剩余子句块的解，如果发现遗漏了规则（2）的情况，应优先处理。

如果前面都是唯一解的情况，遇到了规则（2）的无解情况，那么3SAT无解。

【1】http://blog.sciencenet.cn/blog-340399-928224.html  

2015-11-19