Contradiction in Davis–Putnam–Logemann–Loveland (DPLL) Method?!

Question

As we see on page $10,11$ and $12$ on Google Books we know about Unit Clause (UC) and Pure Literal (PL) in DPLL Algorithms. in the following example if assign value $0$ to variables is prior to assign $1$ to variables, PL and UC is used, but I think just UC is used.

$\{\lnot A \lor B \lor C\}, \{A \lor \lnot B \lor C\}, \{A \lor B \lor \lnot C\}, \{A \lor B \lor C\}$

any idea why our solution is differ with answer sheet that say PL and UC is used?

Edit: I think we have following diagram that in node (3) we can use PL or UC.

Answer 1

Let $\Phi$ the initial set of four clauses as above.

Def 15. A pure literal is a literal $l$ that appears in at least one clause of $\Phi$ while $\lnot l$ doers not appear in any clause of $\Phi$.

Thus, initially, there are no pure literals.

Def 16. A unit clause is a clause with exactly one unknown literal in it.

Thus, initially, there are no unit clauses.

So, you have to apply $DPLL(\Phi)$ selecting e.g. the variable $A$ and branching with:

$DPLL(\Phi|_{A=0})$ and $DPLL(\Phi|_{A=1})$.

For the left branch:

1) $\{ 1∨B∨C \}, \{ 0∨¬B∨C \}, \{ 0∨B∨¬C \}, \{ 0∨B∨C \}$.

Now I suppose you can simplify, according to the rules,:

$1 \lor p \equiv 1$ and $0 \lor p \equiv p$,

to:

1') $\{ 1 \}, \{ ¬B∨C \}, \{ B∨¬C \}, \{ B∨C \}$.

After the first step, again neither pure literals nor unit clauses in this branch.

Then we can go on with $B$; for $B=0$ we have:

1'1) $\{ ¬C \}, \{ C \}$

and for $B=1$:

1'2) $\{ C \}$.

Now we can apply either PL or UL, satisfying this branch.

For the right branch:

2) $\{ 0∨B∨C \}, \{ 1∨¬B∨C \}, \{ 1∨B∨¬C \}, \{ 1∨B∨C \}$.

Simplifying again, we have:

2') $\{ B∨C \}, \{ 1 \}, \{ 1 \}, \{ 1 \}$.

Here we can apply the Pure-Literal rule setting both $B$ and $C$ to $1$, proving again that the formula is SAT.