3SAT什么情况下无满足解？

姜咏江

3-SAT无满足解的情况非常多。在求解过程中如果能够及时地判断出无满足解，无疑会节省出很多计算时间。

用分段子句消去法在求解中出现以下几种情况，就不用再往下浪费时间了。

1.      子句块有8个子句；

2.      两变量已经定值，要设定的动态块一个变量有0和1不同的值出现；

3.      有一个变量值已经确定，要设定的2个变量值出现了｛00、10、01、11｝这4种值。

下图是在求解中出现的3种无解情况。这3种情况都无法确定变量的取值（黄色位置）。绿色部分表示子句已被消去。

3－SAT无解情况

2015-10-19