1
$\begingroup$

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
    http://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.2012-03-09
  • 0
    @martini: Ah, that makes sense! If you make that an answer I will accept it.2012-03-09
  • 0
    Florian gave the answer already.2012-03-09

1 Answers 1

2

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.