Horn-SAT forward-chaining algorithm

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.