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!
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.