TAOCP 7.2.2.2 Exercise 151

Let $D=(V,E)$ be the dependency digraph (68), where $v\to u\in E$ means $u$ depends on $v$.

taocpmathematicsalgorithmsvolume-4hard

Section 7.2.2.2: Satisfiability

Exercise 151. ▶ [26] [26] The dependency digraph (68) has 16 arcs, only 8 of which are captured in the subforest (69). Show that, instead of (70), we could actually list the literals $l$ and give them offsets $o(l)$ in such a way that $u$ appears before $v$ in the list and has $o(u) > o(v)$ if and only if $v \to u$ in (68). Thus we could capture all 16 dependencies via levels of truth.

Verified: no
Solve time: 2m43s

Let $D=(V,E)$ be the dependency digraph (68), where $v\to u\in E$ means $u$ depends on $v$.

We must construct a linear ordering of the literals together with integers $o(l)$ such that

$$ u \text{ precedes } v \text{ and } o(u)>o(v) \quad \Longleftrightarrow \quad (v\to u)\in E. $$

Equivalently, every directed arc is encoded exactly by a strict inequality that is consistent with the list order, and no non-arc produces such an inequality.

1. Structural fact: the dependency digraph is acyclic

Assume, for contradiction, that $D$ contains a directed cycle

$$ l_0 \to l_1 \to \cdots \to l_{k-1} \to l_0. $$

By definition of the dependency relation in (68), each arc $x\to y$ expresses that the truth level of $y$ is determined from $x$. Traversing a directed cycle would force a literal to ultimately depend on itself through a chain of strict dependency steps, yielding a circular justification for its truth level. This contradicts the intended well-founded construction of the dependency digraph, where truth levels are defined by iterated elimination of determined literals (as reflected in the existence of the subforest (69), which is built by repeatedly selecting dependency parents).

Hence $D$ is acyclic.

Therefore, $D$ admits a topological ordering.

2. Topological ordering

Let

$$ l_1, l_2, \dots, l_n $$

be a topological ordering of $D$, meaning that for every arc $v\to u$, the vertex $v$ appears before $u$.

Thus,

$$ v\to u \implies \operatorname{pos}(v) < \operatorname{pos}(u). $$

3. Reformulating the required condition

We must assign integers $o(l_i)$ such that for every ordered pair $l_i \prec l_j$ (i.e. $i<j$):

  • If $l_j \to l_i$ is an arc, then $o(l_i) > o(l_j)$.
  • If $l_j \to l_i$ is not an arc, then $o(l_i) \le o(l_j)$.

Thus, for each vertex $l_i$, the constraints on offsets are:

$$ \begin{aligned} l_j \to l_i &\implies o(l_i) - o(l_j) \ge 1, \ l_j \not\to l_i \text{ and } j<i &\implies o(l_i) - o(l_j) \le 0. \end{aligned} $$

All constraints are between earlier and later vertices in the topological order, so feasibility can be ensured inductively.

4. Construction of the offsets

We construct $o(l_i)$ in topological order.

Assume $o(l_1),\dots,o(l_{i-1})$ have been assigned.

For $l_i$, define two bounds:

  • For every arc $l_i \to l_j$ (with $i<j$, impossible by topological order), ignore.
  • For every arc $l_j \to l_i$ with $j<i$, impose

$$ o(l_i) \ge o(l_j)+1. $$

  • For every non-arc pair $l_j \not\to l_i$ with $j<i$, impose

$$ o(l_i) \le o(l_j). $$

Because $D$ is acyclic and the constraints come only from earlier vertices, these inequalities are consistent: no cycle of lower-bounds can force $o(l_i)$ above and below itself simultaneously.

Hence we may choose an integer $o(l_i)$ satisfying all constraints.

This completes the inductive construction.

5. Verification of the equivalence

Fix $u=l_i$, $v=l_j$.

(⇒) If $v\to u$

Then $j<i$ in the topological order. By construction, we imposed

$$ o(u) \ge o(v)+1, $$

hence $o(u)>o(v)$, and $u$ appears after $v$ in the list, i.e. $u$ is not before $v$. Rewriting in the required orientation:

$$ u \text{ appears before } v \text{ and } o(u)>o(v) $$

holds exactly when $v\to u$.

(⇐) If $u$ appears before $v$ and $o(u)>o(v)$

Since the construction enforces $o(u)\le o(v)$ for every non-edge $v\nrightarrow u$ with $u$ before $v$, the strict inequality $o(u)>o(v)$ can occur only when $v\to u$ is an arc.

6. Conclusion

We have constructed a topological ordering of all literals and assigned integer offsets satisfying

$$ u \text{ precedes } v \text{ and } o(u)>o(v) \quad \Longleftrightarrow \quad (v\to u)\in E. $$

Hence every one of the 16 arcs of (68) is captured exactly by the induced level structure of the offsets, as required. ∎