# Understanding HORNSAT… all variables true?

I'm trying to understand the problem of HORNSAT: given a set of Horn clauses, is there a satisfying assignment. A Horn clause has the form $(x_1 \wedge x_2 \wedge \cdots x_k) \rightarrow v$ where all variables appear positively. What I don't understand is why we can't just set all variables to true, since we never have $\dots \rightarrow \neg v$.

Perhaps the easiest way for me to understand this would be to see an unsatisfiable instance of HORNSAT.

• en.wikipedia.org/wiki/Horn_clause says you only gave the form of a definite Horn clause. Clauses of the form $\neg x_1 \vee \cdots \neg x_k$ (without a positive literal as in your case) are also Horn clauses. And for example $\{x_1, \neg x_2, x_1 \to x_2\}$ is an unsatisfiable instance. – martini Mar 9 '12 at 14:13
• @martini: Ah, that makes sense! If you make that an answer I will accept it. – Max Mar 9 '12 at 14:18
• Florian gave the answer already. – martini Mar 9 '12 at 14:21

Horn clauses can have one positive literal $$\neg x_1 \vee \neg x_2 \vee ... \vee \neg x_n \vee v$$ (which are equivalent to the implication you wrote) or none at all: $$\neg x_1 \vee \neg x_2 \vee ... \vee \neg x_n$$ (also called a "goal clause") and if a goal clause is present, setting all variables to true does not work.