CODEWITHSUNDEEP
algorithmlogicsatisfiabilitysat
user5912880
user5912880

Reputation:

DPLL and Satisfiablity Examples?

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?

Upvotes: 2

Views: 2323

Answers (1)

max taldykin
max taldykin

Reputation: 12908

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.

Upvotes: 4

Related Questions