# Resolution and what it means to derive the empty set

When using resolution, if the empty set {Ø} is derived from a formula like {¬x,¬y} {x,y}, does that mean the formula is unsatisfiable?

If this is the case, why is {x,y},{¬x,¬y},{x,¬y} satisfiable, and

{x},{¬x},{x,y,z,w} is not satisfiable?

• 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.
– D.W.
Commented Nov 17, 2013 at 1:40
• I have now edited. Commented Nov 17, 2013 at 12:55
• $\{x,y\}, \{\neg x, \neg y\}$, $\{x, \neg y\}$ is satisfiable because the assignment $x=\mathrm{true}$, $y=\mathrm{false}$ (or vice-versa) satisfies it. $\{x\}, \{\neg x\}, \mathrm{anything}$ is unsatisfiable because the first clause requires $x$ to be true and the second requires it to be false. Commented Nov 17, 2013 at 18:46
• {Ø} is not the empty set. Commented Jan 23, 2014 at 9:03

A CNF (in Conjunctive normal form) formula, $F$, can be considered as a set of clauses, eg : $F=\{C_1,C_2 \ldots C_m\}$ and each clause can be regarded as a set of literals, eg : $C_1=\{x,y\}, 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=\{\varnothing, C_1 \ldots\}$ 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=\{x\}$ and $C_4=\{\lnot x\}$ is the empty clause $\varnothing=\{\}$.

• Thanks, that cleared it up a bit more, but why is the first clause satsfiable, but not the second? Commented Nov 17, 2013 at 14:04
• 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. Commented Nov 17, 2013 at 14:09
• both the clauses i suggested are not satisfiable check Commented Nov 17, 2013 at 14:10

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.

This is very old post, but I got same question by myself and luckily I've found valid answer so I just write. As I'm not professional pure academic person with respsect to logic, this might be too informal.

I understand the resolution rule by followings.

$$\frac{a \vee p \quad \neg p \vee b}{a \vee b}$$ $$\equiv (a \vee p) \wedge (b \vee \neg p) \rightarrow a \vee b \text{ is tautology}$$

## Not all tautology is empty clause

Note that not every tautology returned by resolution are empty clause. Let's see some examples.

$$\frac{p \vee q \quad \neg p \vee \neg q}{p \vee \neg p}$$

Although resolution rule generated tautology, but $$p \vee \neg p$$ is not an empty clause. It's just one of tautologies.

## Empty clause is only occured with the contradictive literals

The moment that resolution rule returns empty is only for opposite clauses with a single literal(ex: $$p$$ and $$\neg p$$). There is a way to comprehend 'empty clause' situation.

$$\frac{false \vee p \quad false \vee \neg p}{false \vee false}$$

It looks silly, but is still valid since $$false \vee p \equiv p$$ and $$false \vee \neg p \equiv \neg p$$. My notation for understanding resolves this vagueness. Just replace the literals in resolution rule with proper symbols:

$$(false \vee p) \wedge (false \vee \neg p) \rightarrow false \text{ is tautology}$$

It still looks weird, but at least it's defintely true, because the proposition $$false \rightarrow false$$ is tautology. Therefore the result of the resolution rule itself doesn't say anything about prior inputs directly.

But we all know that we start from CNF, and we all know $$p \wedge \neg p$$ is $$false$$ which isn't satisfiable. Since the only case when it gives empty clause is such contradictive situation, we know empty clause implies unsatisfiability.

### Example 1

1. Resolve 1st clause $$x \vee y$$ with 2nd one $$\neg x \vee \neg y$$, get $$x \vee \neg x$$ by removing $$y$$ from them.
2. Resolve 1st clause $$x \vee y$$ with 3rd one $$x \vee \neg y$$, get $$x$$ by removing $$y$$ from them.
3. Resolve 2nd clause $$\neg x \vee \neg y$$ with 3rd one $$x \vee \neg y$$, get $$\neg y$$.
4. Resolve $$x \vee \neg x$$ with $$x$$ which just repetively returns $$x$$.
5. Resolve $$x \vee y$$ with $$\neg y$$ which again returns $$x$$.
6. Remains are also same- just generate the clause that already exists.
7. No empty clause, and satisfiable.

### Example 2.

1. Resolve 1st clause $$x$$ with 2nd one $$\neg x$$ and tada empty clause, which tells that given CNF is unsatisfiable.
• The empty clause is not a tautology, it's a contradiction! You cannot satisfy the empty clause, while $p \lor \bar{p}$ is satisfied by every truth assignment. Commented Jan 1 at 15:34