SAT with DPLL algorithm: Why is this not correct?

81 Views Asked by At

I've got an exam soon and have problems understanding a specific error when performing the DPLL algorithm by hand:

We use 2 additional rules for the algorithm: One literal rule (OLR) and pure-literal rule (PLR)

I have the following clauses :

{ { ¬ s, ¬ q}, {¬ t, ¬ s} }

Why is it uncorrect to say:

PLR| s= false

{}

​Thank you!

1

There are 1 best solutions below

2
On

That should be perfectly acceptable!

$s$ is indeed a pure literal, and by setting it to false, all clauses have been satisfied, so you are left with an empty clause set.

Or: what is the same thing: all clauses with the pure literal can be removed from the clause set, leaving you with the empty clause set.

You could of course also say that $q$ and $t$ are pure literals, and that the clauses with them in it can be removed, which would likewise result in an empty clause set.