# 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. – Raphael Jun 21 '16 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. – Kyle Jones Jun 21 '16 at 15:58
• @KyleJones Thanks, but I think there is a trick in this question. – Sara PhD Jun 21 '16 at 18:10
• @KyleJones please see my update. – Sara PhD Jun 24 '16 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. – Kyle Jones Jun 24 '16 at 7:30