In satisfiability, what is the difference between the empty clause and the empty clause set?

Question

The empty clause is a clause containing no literals and by definition is false: $c = \{\} = F$

What then is the empty clause set, and why does it evaluate to true?

Answer 1

Remember, we take the disjunction over the elements of a clause, then the conjunction over the entire clause set. So if a clause is empty we take the empty disjunction, and if the entire clause set is empty we take the empty conjunction.

What does it mean to take an empty disjunction or empty conjunction? Let's consider a similar situation. Over the real numbers, what is an empty sum, or an empty product? I claim that an empty sum should be $0$; an empty product should be $1$. Why is this? Clearly, we have:

sum($2,3,4$) + sum($5,6,7$) = sum($2,3,4,5,6,7$)

sum($2,3,4$) + sum($5,6$) = sum($2,3,4,5,6$)

sum($2,3,4$) + sum($5$) = sum($2,3,4,5$)

Now make the second sum empty:

sum($2,3,4$) + sum() = sum($2,3,4$)

So sum() should be $0$. In the same way, product() must be $1$. (You can see this by replacing "sum" by "product" and "+" by "$\times$" in the lines above.)

In general, a commutative, associative binary operation applied on an empty set should be the identity element for that operation.

Now back to your original example.

Since the identity for disjunction is "false" (because false OR x = x and x OR false = x for any x), an empty clause is false.

Since the identity for conjunction is "true" (because true AND x = x and x AND true = x for any x), an empty clause set is true.