3-SAT求解基本方法

姜咏江

分段子句消去法的求解，最关键的是关联段求解。3SAT关联段无解只有3中情况：

（1）出现有8个子句的子句块；

（2）出现了只有一个变量需要确定值，却无值可选的动态块；

（3）在确定了一个变量值之后，出现了4个2SAT子句的动态块，叫全2sat动态块。

3SAT解题中如何排除无解分支？基本方法是：先选择4个同变量值的子句块定值，随时注意避免出现全2sat动态块。

下面我们以实际例子来加以说明。

图1中有变量x6和x8有4个相同的值，不选这个值就会进入到无解分支。因而选择x6＝0、x8＝0。

图1  子句块变量4同值

消去相关子句，出现了有唯一解的动态块（图2中有3个子句的子句块）。

图2  出现了唯一解动态子句块

选定动态块解，并消去相关子句就得到了图3，其中有唯一解的子句块2个。

图3  唯一解的一个子句子句块

消去这两个唯一解子句块，得到图4。图4中除了一个4子句块之外，都是有1个子句或2个子句的子句块。这有4个子句的子句块是由两对互反子句构成的，因而也是多解子句块。

图4  多解的4子句子句块

对于都是多解的子句块或动态子句块都可以设定变量值得到相应的解。如图5所示，可有此3SAT的满足解为000010101*1010***01*。“*”表示可以为0或1。

图5  选择关联子句多的变量值

总结一下，当固定了一个变量之后，有一个、两个子句的子句块总有多解。有三个子句的子句块可能有唯一解或多解；有四、五和六个子句的子句块都可能出现无解或多解的情况，七个子句的子句块只有唯一解。

一般过程：

（1）先寻找唯一解或可能无解的子句块，若有无解子句块则关联段无解。进而3SAT无解。

（2）设定值时应避开无解情况。

（3）最后处理都是多解的关联子句块，可设定关联变量值使消去的子句最多。

定理：变量4同值不取，则发生无解。

此定理证明留给读者如何？（参考【1】定理8）

2015-11-18

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