Resolution and what it means to derive the empty set

When using resolution, if the empty set is derived from a formula like , does that mean the formula is unsatisfiable? If this is the case, why is ,, satisfiable, and ,, is not satisfiable?

$\begingroup$ What's your question exactly? Which formula are you trying to test whether it is satisfiable? Sorry, I can't understand your question. I encourage you to edit it to explain your question more clearly -- right now I find it very difficult to follow what you are asking. $\endgroup$

$\begingroup$ $\, \$, $\$ is satisfiable because the assignment $x=\mathrm$, $y=\mathrm$ (or vice-versa) satisfies it. $\, \, \mathrm$ is unsatisfiable because the first clause requires $x$ to be true and the second requires it to be false. $\endgroup$

4 Answers 4

To complete the Kyle's answer:

A CNF (in Conjunctive normal form) formula, $F$, can be considered as a set of clauses, eg : $F=\$ and each clause can be regarded as a set of literals, eg : $C_1=\, C_2=\<\lnot x, \lnot y\>$.

If $F=\varnothing$ i.e. $F$ is the empty set and does not contain any clause then $F$ is satisfiable (=tautology).

If $F=\$ i.e. $F$ contains the empty clause then $F$ is not satisfiable. The empty clause can be obtained by the resolution rule eg : the resolvent of $C_3=\$ and $C_4=\<\lnot x\>$ is the empty clause $\varnothing=\$.

$\begingroup$ Thanks, that cleared it up a bit more, but why is the first clause satsfiable, but not the second? $\endgroup$

$\begingroup$ I think you are confusing clause and formula : your first formula is satisfiable because you can't infer the empty clause by the resolution rule. $\endgroup$

You seem to be trying to describe and use the resolution proof system. Two points:

1. The resolution rule is only applied to two clauses at a time. The resulting clause, the resolvent, can be added to the list of propositional clauses and used in future inferences. But a single resolution inference only ever involves two clauses.
2. You can only remove one pair of complementary literals per invocation of the resolution rule. So while (x,y) (-x, -y) -> (y -y) is a valid inference, albeit tautological, (x,y) (-x, -y) -> Ø is not a valid inference.

To address why the first example is satisfiable but the second is not, it may be helpful to informally think about what's going on geometrically.

The set of all truth-assignments may be represented as the n-cube, or Boolean poset $B_n$. Every literal corresponds to a distinct (n-1)-face; each positive literal corresponds to the filter of a distinct rank 1 element and each negative literal corresponds to the ideal of a distinct rank n-1 element.

If a k-clause encodes the set of all truth-assignments that satisfy it, its dual encodes the (n-k)-face of all truth-assignments that do not satisfy it. (Equivalently, if an input in CNF represents the intersection of unions of maximal ideals and filters of $B_n$, its dual represents the union of closed intervals.) Resolution on the dual input essentially glues unsatisfiable faces together.

Thus, if you can produce the empty clause via resolution, you have shown that the set of unsatisfying faces can be glued together to produce the n-cube itself. Why? Because a 0-clause must be unsatisfied by an (n-0)-face of assignments, which is all of them.

In the dual formulation of your first example, you have three 0-faces of the 2-cube. Obviously three 0-faces cannot cover all four 0-faces of the 2-cube, so the collection must be satisfiable.

In the dual formulation of your second example, you have two 3-faces and one 0-face of the 4-cube. Since we can glue the two 3-faces together to form the 4-cube, the collection must be unsatisfiable; the 4-face will absorb all other subfaces since it entails them, rendering them redundant.