博文
简单求3-SAT解DPLL方法与子句消去法比较
|||
SAT问题求解的DPLL算法是一种带回溯的深度优先搜索，其方法简单例子如下：
a' | b' | c | a' | b' | c | a' | b' | c | a' | b' | c | |||
a' | b | c' | a' | b | c' | a' | b | c' | a' | b | c' | |||
a' | b | c | a' | b | c | a' | b | c | a' | b | c | |||
a | b' | c' | a | b' | c' | a | b' | c' | a | b' | c' | |||
a | b' | c | a | b' | c | a | b' | c | a | b' | c | |||
a | b | c' | a | b | c' | a | b | c' | a | b | c' | |||
a | b | c | a | b | c | a | b | c | a | b | c | |||
a' | b' | a' | b | a | b' | a | b | c |
（1） （2） （3） （4）解
上面的共有7个3-SAT子句，灰色底纹表示求解中屏蔽的子句，没有底纹的子句是设定变量值要考察的子句。考察的方法是设定上层搜索值后，确定叶的值要寻找非屏蔽子句中上层全是反文字的，并有叶文字的子句。叶文字矛盾，此次搜索不是解，不矛盾就得到了叶的确定值，从而得到满足解。下面有顺序标号所列的是求解步骤。
DPLL算法复杂度：
每次设定叶c的值，都要查遍a至c所有文字。因为总是查询原3-SAT，搜索节点前两步为7+4+2=13，后两步分别为7+3+2=12和7+3+1=11。搜索次数为22=4。若是最坏无解的情况，这3个变量的3-SAT要查询14*4=56次。
下面我们来看子句消去法求解：
子句消去法求变量值是考察各级子句块变量的同种文字数量，这个3-SAT子句变量相同，只要看每次得到的子句块中变量文字数量是否有全块的子句数的一半，正反文字数相等，无解，不然取其文字为变量值。此例有解。
a' | b' | c |
| b' | c |
|
| c | ||
a' | b | c' |
| b | c' |
|
|
| ||
a' | b | c |
| b | c |
|
|
| ||
a | b' | c' |
|
|
|
|
|
| ||
a | b' | c |
|
|
|
|
|
| ||
a | b | c' |
|
|
|
|
|
| ||
a | b | c |
|
|
|
|
|
| ||
a |
| a | b | a | b | c |
（1） （2） （3） 解
第（1）步，有4个正文字a，消去有a的子句。剩余2-SAT子句。
第（2）步，有2个正文字b，消去子句。剩余1-SAT子句。
第（3）步，有一个正文字c，消去子句。没有了剩余子句。
子句消去法算法复杂度：
三步查询次数为7+3+1=11次。如果是最坏无解的情况，只要查询8次即可。
以上所举的例子只是一种简单的唯一解情况，虽然不能包括子句块相互关联的情况，但可以反映出子句消去法较DPLL方法的超快特性。
https://blog.sciencenet.cn/blog-340399-1021831.html
上一篇：限位数——一个人们不曾研究的领域
下一篇：我应不应该去踢美国克雷数学研究所的门？
