TAOCP 7.2.2.1 Exercise 264
Let the items be arranged in the circular doubly linked list headed by node $0$, with the active items forming a linear order when read from $i = \mathrm{RLINK}(0)$ forward.
Section 7.2.2.1: Dancing Links
Exercise 264. [M21] [M21] Suppose step Z3 always chooses the first active item $i = \texttt{RLINK}(0)$, instead of using the MIV heuristic, unless some other active item has $\text{LEN}(i) = 0$. Prove that Algorithm Z will then output an ordered ZDD.
Verified: yes
Solve time: 1m09s
Solution
Let the items be arranged in the circular doubly linked list headed by node $0$, with the active items forming a linear order when read from $i = \mathrm{RLINK}(0)$ forward. Write this order as
$i_1, i_2, \dots, i_n,$
where $i_1 = \mathrm{RLINK}(0)$ and $i_{k+1} = \mathrm{RLINK}(i_k)$.
The modified step Z3 selects $i_1$ unless there exists an active item $i$ with $\mathrm{LEN}(i)=0$, in which case such an item is selected instead. Since $\mathrm{LEN}(i)=0$ immediately forces failure of the branch in Algorithm Z, this selection does not produce new continuations in the search; it only terminates a dead subproblem.
Consider any recursive call generated by Algorithm Z under this rule. The active items at that point form a subset of the original ordered list, preserved in their relative order by the dancing-links operations (12) and (14), since these operations only delete and restore nodes without reordering the horizontal list pointers. Therefore, the active items remain totally ordered by the restriction of $\mathrm{RLINK}$.
Define the invariant that at every invocation of Z, the next item chosen for branching is the smallest active item in the fixed order induced by repeated application of $\mathrm{RLINK}$ starting at $0$. This invariant holds at the root by construction of step Z3. Assume it holds at a recursive call. The algorithm removes all options containing the chosen item $i_k$, but the linking structure of remaining items preserves the relative order of all other items, so the next call again has a well-defined first active item $\mathrm{RLINK}(0)$ in the restricted list, which is the smallest remaining element in the original ordering. If an item with $\mathrm{LEN}(i)=0$ exists, it is removed immediately as a dead branch and does not lead to further recursive branching, so it does not affect the ordering of choices along successful paths.
Along any root-to-leaf path that produces a solution, each recursive level selects an item $i_{k_j}$ that is the first remaining element of the active list at that time. After $i_{k_j}$ is covered, it is removed from the active list, and all subsequent choices are made from items strictly to its right in the original $\mathrm{RLINK}$ order. Hence if $i_{k_a}$ is chosen before $i_{k_b}$ in a solution path, then $k_a < k_b$, since $i_{k_b}$ lies to the right of $i_{k_a}$ in the fixed ordering when it is selected.
Therefore every solution corresponds to a sequence of item choices in strictly increasing order with respect to the initial $\mathrm{RLINK}(0)$ ordering. This implies that in the ZDD produced by Algorithm Z, every path from the root to the terminal node respects a fixed variable order, and no item appears out of order along any path.
This satisfies the definition of an ordered ZDD: all decision nodes are labeled by items in a consistent total order, and along every directed path from root to terminal, the labels appear in strictly increasing order.
This completes the proof. ∎