DPLL algorithm from 16.02.2022 - backtracking?

Question

At first, the unit clause {x3} demands the assignment x3 := true, which propagates to the other clauses as follows: 

{x0, ¬b, ¬c}, {¬x0, b}, {¬x0, c} 

{¬x0, ¬x1}, {x1, x0} 

{x1, ¬x2, ¬a}, {¬x1, x2}, {x2, a}

{¬x2, c}, {x2, ¬c} 

We now have four clauses with only two literals and an occurrence of x0, so that we make the case split x0 := true (instead of false as per the solution), which yields the following clauses:

{b}, {c} 

{¬x1}

{x1, ¬x2, ¬a}, {¬x1, x2}, {x2, a}

{¬x2, c}, {x2, ¬c}

The new unit clauses {b}, {c} , {¬x1} demand assignments of   b := c:= true and x1 := false. Propagating this yields:

{}, {} 

{}

{¬x2, ¬a}, {x2, a}

{x2}

Do we backtrack here and make x0 := false due to the empty clauses and then continue? 

Proceeding otherwise means x2 := true and the following:

{¬a}

{}

which demands a:= false

The final assignments obtained are x3 := x0 := x2 := b :=c := true and x1 := a := false 

(compared, the exam solution : x3 := x1 := x2 := c := true and x0 := b := false , a:= arbitrary)

Answer 1

When assigning  b := c := true and x1 := false, the clauses {b}, {c},{¬x1} do not become empty clauses, the clauses are just removed. What happens precisely is the unit clause propagation rule. Therefore, the only way to proceed is to assign x2:=true as another unit clause propagation, and the get the model.

Bytheway, looking at the BDD of the clause set shows the possible models you could get:

Comments

Thank you Professor. So, both these are valid models. Is my understanding correct?

---

Right, both are satisfying assignments, and each one is as good as the other one.