= Horn-SAT forward-chaining algorithm
{c}
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\land\cdots\land 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.
Back to article page
