博文
子句消去法与DPLL方法求SAT满足解比较
|||
子句消去法与DPLL方法求SAT满足解比较
Davis, Logemann, Loveland (1962) had developed this algorithm. Some properties of this original algorithm are:
· It is based on search.
· It is the basis for almost all modern SAT solvers.
· It DOES NOT use learning and chronological backtracking (introduced in 1996).
An example with visualization of a DPLL algorithm having chronological backtracking:
(a’+b+c)(a+c+d)(a+c+d’) (a+c’+d) (a+c’+d’) (b’+c+d’) (a’+b+c’) (a’+b’+c) (1)
1 a
2 0/
3 b
4 0/
5 c
6 0/
7 ■
a－0→b－0→c－0→F 通过a+c+d→d=1, 通过a+c+d’→d=0,产生矛盾；
1 a
2 0/
3 b
4 0/
5 c
6 0/ 1
7 ■ ■
回溯到c
a－0→b－0→c－1→F 通过a+c’+d→d=1, 通过a+c’+d’→d=0,产生矛盾；
1 a
2 0/
3 b
4 0/ 1
5 c
6 0/ 1
7 ■ ■
回溯到b,另外分支
1 a
2 0/
3 b
4 0/ 1
5 c c
6 0/ 1 0/
7 ■ ■■
a－0→b－1→c－0→F 没有a+b’+和b’+c’+的子句；
1 a
2 0/
3 b
4 0/ 1
5 c c
6 0/ 1 0/ 1
7 ■ ■■■
a－0→b－1→c－1→F 还是a+c’+d→d=1, 通过a+c’+d’→d=0,产生矛盾；
1 a
2 0/ 1
3 b
4 0/ 1
5 c c
6 0/ 1 0/ 1
7 ■ ■■■
回溯到a,另外分支
a－1→b－0→c－1→F 没有a’+c+推出d；
1 a
2 0/ 1
3 b b
4 0/ 1 0/ 1
5 c c ■ c
6 0/ 1 0/ 1 1
7 ■ ■■■ △
a－1→b－1→c－1→T 有a’+b’+c推出c=1；a’+c’+d推出d=1；
最后结果是a=1,b=1,c=1,d=1
子句消去法：
用k阶子句变量有2k-1个“0”或“1”就可确定变量值即可。
表1 唯一解a=1
1 |
|
|
|
a | b | c | d |
0 | 1 | 1 |
|
1 |
| 1 | 1 |
1 |
| 1 | 0 |
1 |
| 0 | 1 |
1 |
| 0 | 0 |
| 0 | 0 | 1 |
0 | 1 | 0 |
|
0 | 0 | 1 |
|
表2 唯一解 b=1,c=1
1 | 1 | 1 |
|
a | b | c | d |
0 | 1 | 1 |
|
| 0 | 0 | 1 |
0 | 1 | 0 |
|
0 | 0 | 1 |
|
表3 得唯一解a=1 b=1 c=1 d=1
1 | 1 | 1 | 1 |
a | b | c | d |
https://blog.sciencenet.cn/blog-340399-1020181.html
上一篇：包括批评我的那些关心子句消去法的人都是我珍贵的朋友
下一篇：论文参考文献自引就一定不好吗？
