by Yu Feng
DPLL(F):
F ← BCP(F)
if F = ⊤ return true. // 1
if F = ⊥ return false
p ← choose variable // 2
return DPLL(F[p := true]) || DPLL(F[p := false]) // 3
DPLL Drawbacks
View more
CDCL(F)
A ← {}
if BCP(F,A)=conflict then return ⟘
level ← 0
while hasUnassignedVars(F)
level ← level + 1
A ← A ∪ { DECIDE(F, A) }
while BCP(F,A) = conflict
⟨b, c⟩ ← ANALYZECONFLICT()
F ← F ∪ {c}
if b < 0 then return ⟘
else BACKTRACK(F, A, b)
level ← b
return ⟙
F = { c1,c2,c3,c4,c5,c6 }
c1: ¬x1 ⋁ x2 ⋁ ¬x4
c2: ¬x1 ⋁ ¬x2 ⋁ x3
c3: ¬x3 ⋁ ¬x4
c4: x4 ⋁ x5 ⋁ x6
c5: x7 ⋁ ¬x5
c6: ¬x6 ⋁ x7 ⋁ ¬x8
CDCL(F)
A ← {}
if BCP(F,A)=conflict then return ⟘
level ← 0
while hasUnassignedVars(F)
level ← level + 1
A ← A ∪ { DECIDE(F, A) }
while BCP(F,A) = conflict
⟨b, c⟩ ← ANALYZECONFLICT()
F ← F ∪ {c}
if b < 0 then return ⟘
else BACKTRACK(F, A, b)
level ← b
return ⟙