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**)**