I'm having trouble understanding how to use the resolution rule to prove if a statement is satisfiable or unsatisfiable.
I watched this course lecture on propositional resolution and unsatisfiability (linked with a time stamp to skip to the part in question):
"5.4 - Resolution Method - Propositional Resolution - [Introduction To Logic] By Michael Genesereth" https://www.youtube.com/watch?v=IpixwNupBIs#t=2m21s
For those that don't want to watch the video, my understanding is that he is saying that for a statement in conjunctive normal form (CNF) we can test whether the statement is satisfiable by repeatedly applying the simplifying resolution rule:
If there is a pair of clauses of the form $$(a \vee X)$$ $$(\neg a \vee Y)$$ this can be replaced by a single clause $$(X \vee Y)$$
The claim is that a statement is unsatisfiable if and only if repeated application of this rule leads to an empty clause.
But this doesn't make sense to me. I think there are some important details that are left out. For instance in the example given in the video, consider the statement with the clauses
- $(p \vee q)$
- $(p \vee \neg q)$
- $(\neg p \vee q)$
- $(\neg p \vee \neg q)$
By inspection, this is unsatisfiable. But let's find this using the resolution rule, following along with the video...
Applying the resolution rule on pair 1,2 gives: $p$
Then applying the resolution rule on pair 3,4 gives $\neg p$
So now we just have the clauses $p, \neg p$, which after applying the resolution rule one more time gives the empty clause.
That is how the example goes in the video. But look what happens if we apply the rule in another order:
Applying the resolution rule on pair 1,4 gives: $q \vee \neg q$
Then applying the resolution rule on pair 2,3 gives $\neg q \vee q$
So now we are just left with two clauses which are tautologies. So we simplified the statement to just $\top$. So by this order, it claims the statement is satisfiable.
Clearly something is wrong. What am I misunderstanding? Or is the course lecture leaving out something crucial?