DPLL algorithm from August 31, 2021 - Multiple solutions?

Question

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

{x0, ¬b}, {x0, ¬c}, {b, c, ¬x0}
{x0, ¬x1}, {x1, ¬a, ¬x0}, {a, ¬x1}
{x1, ¬b}

-> x0 := true

{b, c} {x1, ¬a}, {a, ¬x1} {x1, ¬b}

-> x1 := true

{b, c}
{a}

->  b := true

{a}

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

(compared to the exam solution: x0 := b := c := x1 := false, a := arbitrary)

Is my solution correct?

Answer 1

Yes, I think it is correct. However, in the last step, you should have first assigned a true, since that is a unit clause. Since a propositional logic formula has usually many satisfying assignments, there are typically also many solutions for SAT solving.