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.

  • 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.