TAOCP 7.1.1 Exercise 47
Let $j \prec k$ be a relation on ${1,\dots,n}$ as in Algorithm 2.
Exercise 47. [20] Given a sequence of relations $j \prec k$ with $1 \le j, k \le n$ as in Algorithm 2.2.3T (topological sorting), consider the clauses
$$x_{j_1} \wedge \cdots \wedge x_{j_b} \Rightarrow x_{j_b} \qquad \text{for } 1 \le k \le n,$$
where ${j_1, \ldots, j_t}$ is the set of elements such that $j_s \prec k$. Compare the behavior of Algorithm C on these clauses to the behavior of Algorithm 2.2.3T.
Verified: yes
Solve time: 1m34s
Solution
Let $j \prec k$ be a relation on ${1,\dots,n}$ as in Algorithm 2.2.3T, and for each $k$ let ${j_1,\dots,j_b}$ be the set of all indices $j$ such that $j \prec k$. The associated Horn clause is
$$ x_{j_1} \wedge \cdots \wedge x_{j_b} \Rightarrow x_k. $$
Interpreting each $x_k$ as a Boolean variable, Algorithm C processes such clauses by repeatedly applying the rule that whenever all antecedents of a clause are true, its consequent must be set to true, continuing until no further changes occur.
Initially, a variable $x_k$ becomes eligible to be set to $1$ precisely when its antecedent set ${j_1,\dots,j_b}$ is empty. This occurs exactly for those $k$ with no predecessors under $\prec$, so these indices are forced to become true immediately. After such a variable $x_k$ is set to $1$, it may satisfy antecedents of other clauses, possibly enabling further variables to be set to $1$ in subsequent stages.
Define a stage ordering by letting a variable $x_k$ become true at the first moment when all $x_j$ with $j \prec k$ are already true. This condition matches the defining property of a topological ordering produced by Algorithm 2.2.3T, since that algorithm outputs vertices only after all predecessors have been output.
Inductively, suppose the variables set to true after $t$ applications of the propagation rule are exactly those vertices whose predecessors lie entirely among vertices already set to true in earlier stages. Then every remaining clause whose antecedents are already true forces its consequent at the next application of Algorithm C, and no variable outside this closure condition can be set earlier.
Algorithm 2.2.3T constructs a linear extension of $\prec$ by repeatedly selecting a vertex with no remaining predecessors. Algorithm C produces the same stratification: at each step, the variables newly forced to $1$ are exactly those vertices whose predecessors have all been forced earlier, which is the same selection criterion expressed in Boolean form.
Thus both procedures generate the same dependency-driven ordering of the vertices, differing only in presentation: Algorithm 2.2.3T outputs the order explicitly, while Algorithm C derives it implicitly as the fixed point of Horn-clause propagation under the implication system defined by $\prec$.
This completes the proof. ∎