DPLL and Satisfiablity Examples?

2
votes

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?

{~A \/ B \/ C}, {A \/ ~B \/ C}, {A \/ B \/ ~C}, {A \/ B \/ C}

In this example wrote by using two of them (PL and UC). why two of them is selected? any idea?

1
algorithmlogicsatisfiabilitysat
You know that backtracking is involved. If the rest was only UP and PL and there would nothing to backtrack to because it wouldn't make any choices that might be wrong. - harold
@harold You can use PL or UC. you can use one of them. - user5915883
@user4249446 of course you can, but you can't only use them, in general. - harold
@harold so you agree with me that in this specific example you can use both of them? - user5915883

1 Answers

4
votes

Here is how DPLL could be used to solve your example formula:

  • 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.
  • To apply splitting rule select some literal, e.g. A.
    • Set A=0 and propagate. This will result in
      {1 \/ B \/ C}, {0 \/ ~B \/ C}, {0 \/ B \/ ~C}, {0 \/ B \/ C}
      == {~B \/ C}, {B \/ ~C}, {B \/ C}
    • Unit propagation and pure literal are still not applicable.
    • Apply splitting rule for the next literal B.
      • Set B=0 and propagate:
        {1 \/ C}, {0 \/ ~C}, {0 \/ C}
        == {~C}, {C}
      • This formula consists of two unit clauses so it is possible to apply unit propagation, which results in {} so we backtrack.
      • Set B=1 and propagate. {0 \/ C}, {1 \/ ~C}, {1 \/ C}
        == {C}
      • Again, unit propagation is applicable, but now results in empty formula which is trivially satisfiable.

Which of Unit Clause (UC) or Pure Literal (PL) is used to solve this specific example?

Unit Clause propagation is used to solve this example. And due to symmetry of the formula, choosing splitting literals in different order will lead to the same result.