Horn clause

A Horn clause is a disjunction of literals containing at most one positive literal. It can be read as an implication whose antecedent is a conjunction of variables.

A first-order clause containing at most one positive first-order literal. A clause with exactly one positive literal is definite; with no positive literal it is a constraint or goal clause.

Horn-SAT asks whether a conjunction of Horn clauses is satisfiable.

The Horn-SAT forward-chaining algorithm maintains the set $T$ of Boolean variables already forced true. Write each Horn clause as an implication $a_1\wedge \cdots \wedge a_k\to b$, where the conclusion is either a Boolean variable or false. Start with $T=\varnothing$. Whenever every antecedent belongs to $T$, add the conclusion $b$; if the conclusion is false, report failure.

Every satisfying assignment must make all members of $T$ true: this holds initially and is preserved by each enabled implication. Thus an enabled false conclusion proves that no satisfying assignment exists. If no further Boolean variable can be added and no such failure occurs, interpreting exactly $T$ as true satisfies every Horn clause. It is the least satisfying assignment under inclusion of true Boolean variables.

For example, the clauses $p$, $p\to q$ and $q\to r$ force $T=\{p,q,r\}$. Adding $r\to \mathrm{false}$ makes the instance unsatisfiable. Each Boolean variable enters $T$ at most once. Indexing antecedent occurrences and maintaining a counter per clause permits one update per occurrence, avoiding repeated full scans.