TAOCP 7.1.1 Exercise 48
A Horn clause is a disjunction of literals containing at most one uncomplemented variable.
Exercise 48. ▶ [21] What's a good way to test a set of Horn clauses for satisfiability?
Verified: yes
Solve time: 1m24s
Solution
A Horn clause is a disjunction of literals containing at most one uncomplemented variable. Each clause can be written in implication form as
$$ x_{i_1} \wedge \cdots \wedge x_{i_b} \Rightarrow y $$
where $y$ is either a variable or the constant $0$ (the empty head case corresponds to a purely negative clause). A set of Horn clauses is satisfiable when there exists an assignment of the variables in ${0,1}$ that makes every clause true.
A testing method proceeds by constructing the least assignment forced by the implications. Begin with all variables assigned value $0$. Maintain the set of variables whose value has been changed from $0$ to $1$. For each clause
$$ x_{i_1} \wedge \cdots \wedge x_{i_b} \Rightarrow y $$
the antecedent becomes true exactly when all $x_{i_1}, \ldots, x_{i_b}$ have already been set to $1$. When this occurs and $y$ is a variable, assign $y \leftarrow 1$. When $y = 0$ and the antecedent becomes true, the system is inconsistent and no satisfying assignment exists.
Each assignment step increases the number of variables equal to $1$, and no variable is ever changed back to $0$. Since there are only finitely many variables, the process terminates after finitely many steps at a fixed point where no further clause forces a new assignment.
If the procedure halts due to triggering a clause with head $0$, then some antecedent evaluates to $1$ while the clause requires $0$, so no assignment can satisfy all clauses simultaneously. If the procedure reaches a fixed point without triggering such a clause, consider the resulting assignment $v$. For every clause $x_{i_1} \wedge \cdots \wedge x_{i_b} \Rightarrow y$, either at least one antecedent variable is $0$ under $v$, making the antecedent false, or all antecedent variables are $1$, in which case the construction has already assigned $y = 1$ unless $y = 0$, which would have caused immediate failure. Hence every clause evaluates to true under $v$.
This construction produces an assignment that is minimal with respect to the ordering $0 < 1$ on each variable, since variables are set to $1$ only when forced by a clause and never otherwise. Any satisfying assignment must assign at least the same variables the value $1$, since each such assignment must respect every implication that becomes activated during the process.
The algorithm therefore tests satisfiability by computing this forced fixed point; success of the construction is equivalent to satisfiability of the Horn system. ∎