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?