Can we resolve two variables at a time in CNF resolution

485 Views Asked by At

Are we allowed to resolve two variables at a time in CNF resolution?

For e.g. we have:

what will be the resolution of: $(P \lor \lnot Q \lor R) \land (\lnot P \lor Q \lor R)$

and what will be the resolution of: $(P \lor \lnot Q \lor R) \land (\lnot P \lor Q)$

Thanks, Hakid

1

There are 1 best solutions below

0
On

No! Absolutely not!

Consider: You have $\{A, B \}$ and $\{\neg A, \neg B \}$

If you could resolve two at a time this would result in the empty clause $\{ \}$, which would suggest that the orginal clauses are not satisfiable. But clearly they are, e.g. set $A$ to True and $B$ to False.