title: DPLL and Satisfiablity Examples?
body: <p>We know <code>DPLL</code> algorithm is backtracking + unit propagation + pure literal rule.</p>
  
  <p>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 <code>Unit Clause (UC)</code> or <code>Pure Literal (PL)</code> is used to solve this specific example?</p>
  
  <pre><code>{~A \/ B \/ C}, {A \/ ~B \/ C}, {A \/ B \/ ~C}, {A \/ B \/ C}
  </code></pre>
  
  <p>In this example wrote by using two of them (<code>PL and UC</code>). why two of them is selected? any idea? </p>