Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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.

share|cite|improve this question
2 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
up vote 2 down vote accepted

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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.