子句消去法与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阶子句变量有2^k-1个“0”或“1”就可确定变量值即可。

表1   唯一解a=1

表2  唯一解 b=1,c=1

表3  得唯一解a=1 b=1 c=1 d=1