# How to choose between UC and PL when using the DPLL algorithm?

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.

Update: I think in node (3) we can user PL or UC. Isn't it?

• Note that this question does not seem to have anything to do with AI; it's a pure logics question. Commented Jun 21, 2016 at 9:03
• As far as I can see, you are correct. Assigning variables as you described, false first then backtracking to true if a conflict occurs, you arrive at a solution using only unit propagation. Pure literal elimination is never invoked. This is the case regardless of the variable assignment order as the clause-variable graph is just one big automorphism. Commented Jun 21, 2016 at 15:58
• @KyleJones Thanks, but I think there is a trick in this question. Commented Jun 21, 2016 at 18:10
• @KyleJones please see my update. Commented Jun 24, 2016 at 0:14
• The pure literal rule is applicable to (3), but it never would be applied because the unit rule is always applied first in DPLL. Commented Jun 24, 2016 at 7:30