CODEWITHSUNDEEP
logicsatsatisfiability
grokestray
grokestray

Reputation: 31

Satisfiability with DP and DPLL yields different results

I have the following clauses:

1. {P,Q,~R}
2. {~P,R}
3. {P,~Q,S}
4. {~P,~Q,~R}
5. {P,~S}

I have to prove the satisfiability using DP and DPLL separately. The problem is that I am getting different results for each algorithm. With DP:

1. {P,Q,~R}
2. {~P,R}
3. {P,~Q,S}
4. {~P,~Q,~R}
5. {P,~S}
6. {Q} from 1 and 2

2. {~P,R}
3'. {P,S}
4'. {~P,~R}
5. {P,~S}
7. {P} from 3' and 5

2. {R}
4'. {~R}
8. {}

So it is unsatisfiable. But with DPLL:

1. {P,Q,~R}
2. {~P,R}
3. {P,~Q,S}
4. {~P,~Q,~R}
5. {P,~S}
6. {P} split(P)

2'. {R}
4'. {Q,~R}

7.{Q}

Which would mean it is satisfiable... What did I do wrong?

Upvotes: 0

Views: 266

Answers (1)

Tim
Tim

Reputation: 1098

In the first inference in DP, the resolution rule is not applied correctly. Let's focus of the inference of 6. {Q} from 1 and 2 from 1. {P,Q,~R} and 2. {P,Q,~R}. The assignment of P, Q, and R to false satisfies {P,Q,~R} and {~P,R}, but it does not satisfy {Q} which the inference is are claiming is entailed by the previous two. The possible resolvents of {P,Q,~R} and {~P,R} are:

  • {Q, ~R, R} by resolving on P
  • {P, Q, ~P} by resolving on R

Both of these clauses are always true and are discarded by DP. (Discarding is sometimes called the tautology rule.) These do not entail {Q} as shown in the previous counter example.

Also note that on the DPLL example, you have assigned P, R, Q to true. This is inconsistent with clause 4. {~P,~Q,~R}. Unit propagation needs to be applied exhaustively for this split.

You can find many presentations of DP and DPLL online. Examples: 1, 2. Try to apply the rules consistently and exhaustively.

Upvotes: 1

Related Questions