We know DPLL algorithm is backtracking + unit propagation + pure literal rule.
I have an example. There is one example to solve following Satisfiability problem with DPLL. if assign of "0" to variables is prior to assign "1" to variables, Which of Unit Clause (UC) or Pure Literal (PL) is used to solve this specific example?
$\{\lnot A \lor B \lor C\}, \{A \lor \lnot B \lor C\}, \{A \lor B \lor \lnot C\}, \{A \lor B \lor C\}$
Olympiad Solution is: PL and UC.
Our Solution is just UC.
Who can satisfy me why Olympiad solution is correct ?!
Unit propagation is not possible as there are no unit clauses.
Pure literal rule is not applicable as there is no literals that occur only positively or only negatively.