2SAT Problem: Is it okay to derive the empty clause in this manner?

57 Views Asked by At

If I have: {x,y},{x,z},{y,z},{¬x,¬y},{¬x,¬z},{¬y,¬z}

I can see that through the clause {¬x,¬y}, I will be able to cancel out variables to be left with {z}, however, can I use {¬x,¬z},{¬y,¬z} on {z} to remove it or will that cause a problem as I would have already gotten rid of x and y?

1

There are 1 best solutions below

0
On

When you resolve two clauses $\{x, y \}$ and $\{x', y \}$ to get $y$, you could indeed say that you have 'gotten rid of' $x$ and are 'left with' $y$

But please note that the clauses, and thus the variables within them, never go away. In fact, all you do when resolving clauses is adding more and more clauses to the clause set, and at any point, you can try to resolve any two clauses from that growing clause set. Indeed, you can use the same clause any number of times.

So in answer to your question: yes, you can!