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.

  • 2
    $\begingroup$ 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. $\endgroup$ – martini Mar 9 '12 at 14:13
  • $\begingroup$ @martini: Ah, that makes sense! If you make that an answer I will accept it. $\endgroup$ – Max Mar 9 '12 at 14:18
  • $\begingroup$ Florian gave the answer already. $\endgroup$ – 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.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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