TAOCP 7.1.1 Exercise 51
A correct solution must avoid two mistakes in the previous attempt: 1.
Exercise 51. ▶ [22] A great many two-player games can be defined by specifying a directed graph in which each vertex represents a game position. There are two players, Alice and Bob, who construct an oriented path by starting at a particular vertex and taking turns to extend the path, one arc at a time. During the game starts, each vertex has either been marked A (meaning that Alice wins), or marked B (meaning that Bob wins), or marked C (meaning that the cat wins), or left unmarked.
When the path reaches a vertex $v$ marked A or B, that player wins. The game stops without a winner if $v$ has been visited before, with the same player to move. If $v$ is marked C, the currently active player has the option of accepting a draw; otherwise he or she must choose an outgoing arc to extend the path, and the other player becomes active. (If $v$ is an unmarked vertex with out-degree zero, the active player loses.)
Associating four propositional variables $A^+(v)$, $A^-(v)$, $B^+(v)$, and $B^-(v)$ with every vertex $v$ of the graph, explain how to construct a set of definite Horn clauses such that $A^+(v)$ is in the core of (and only if Alice can force a win when the path starts at $v$ and she moves first; $A^-(v)$ is in the core if and only if Bob can force her to lose in that game; $B^+(v)$ and $B^-(v)$ are similar to $A^+(v)$ and $A^-(v)$, but with roles reversed.
Verified: no
Solve time: 4m18s
A correct solution must avoid two mistakes in the previous attempt:
- It must not treat $A^-$ and $B^-$ as simple dual reachability predicates.
- It must incorporate the effect of $C$-vertices as genuine strategic choices affecting forced outcomes.
- It must justify the construction purely in terms of a monotone Horn fixed-point system without appealing to incorrect cycle elimination arguments.
The key is to encode all four predicates as simultaneously inductive winning conditions in a single product game, rather than attempting to interpret $A^-$ and $B^-$ as logical negations.
1. Reframing the game as a four-valued objective system
Each position consists of a vertex $v$ and a player to move $p \in {A,B}$.
Instead of interpreting $A^-(v)$ and $B^-(v)$ as complements, we interpret all four predicates as positive reachability conditions in different game variants:
- $A^+(v)$: Alice, to move at $v$, can force a state where Alice is declared winner.
- $B^+(v)$: Bob, to move at $v$, can force a state where Bob is declared winner.
- $A^-(v)$: Alice, to move at $v$, can force that Bob is not able to force a win for Bob.
- $B^-(v)$: Bob, to move at $v$, can force that Alice is not able to force a win for Alice.
The crucial correction is that $A^-$ and $B^-$ are not complements. They are independent safety-style winning objectives.
Each predicate is defined by its own Horn system, but all systems share the same graph transitions.
2. State expansion to encode $C$-choices correctly
At a $C$-vertex, the active player has an explicit option:
- move along an outgoing edge $v \to w$, or
- stop and accept draw.
This is not eliminable and must appear as a real choice in the Horn system.
We encode “accept draw” as a special terminal action that does not satisfy any of the four predicates.
Let this be represented by a null successor $\bot$.
Thus every $C$-vertex has effective successors:
$$ \operatorname{Succ}_C(v) = \operatorname{Succ}(v) \cup {\bot}. $$
For all predicates $X \in {A^+, A^-, B^+, B^-}$, we impose:
$$ X(\bot) \text{ is false.} $$
This makes draw a genuine strategic alternative that blocks derivations.
3. Horn principle used
All clauses have the form:
- existential choice (player move): one successful successor is sufficient
- universal constraint only appears when a player is trying to guarantee a property against all opponent replies
A definite Horn clause has the form:
$$ \text{(conjunction of atoms)} \Rightarrow \text{atom}. $$
Thus we encode:
- existential choice as multiple Horn clauses
- universal choice as a single Horn clause with a conjunction in the body
4. Correct clauses for $A^+(v)$
Alice moves.
Winning vertex
If $v$ is marked $A$:
$$ \top \Rightarrow A^+(v). $$
Move transitions
Alice can choose any successor or accept draw only at $C$-vertices.
For every edge $v \to w$:
$$ A^+(w) \Rightarrow A^+(v). $$
At a $C$-vertex, Alice also has the option $\bot$, which never produces $A^+$, so it is irrelevant for derivability.
No additional clause is added.
Out-degree zero unmarked vertices
If $v$ is unmarked and $\operatorname{Succ}(v)=\varnothing$, Alice loses immediately, so no rule derives $A^+(v)$.
5. Correct clauses for $B^+(v)$
Symmetric to $A^+(v)$.
If $v$ is marked $B$:
$$ \top \Rightarrow B^+(v). $$
For every edge $v \to w$:
$$ B^+(w) \Rightarrow B^+(v). $$
No special handling for $C$-vertices is needed beyond the fact that $\bot$ does not contribute.
6. Correct construction of $A^-(v)$
This is the critical correction.
Meaning
$A^-(v)$ means:
Bob (opponent of Alice’s winning objective) can force that Alice does not reach a winning state.
This is not a complement. It is a forcing safety condition.
Thus the correct inductive interpretation is:
- Bob moves at the same vertex set, but with objective “avoid $A^+$”.
We define $A^-$ as the least fixed point of a safety operator.
Winning base cases for $A^-$
If $v$ is marked $B$, Bob already wins, so:
$$ \top \Rightarrow A^-(v). $$
If $v$ is unmarked and has no successors:
$$ \top \Rightarrow A^-(v). $$
Transition rule
Bob moves at positions where Alice would move in $A^+$. Bob wants to ensure Alice cannot force a win.
At a position $v$, Bob can enforce $A^-(v)$ if he has a move to a successor $w$ that is already safe for Bob, i.e. $A^-(w)$.
Thus:
$$ A^-(w) \Rightarrow A^-(v) \quad \text{for each } w \in \operatorname{Succ}(v). $$
This is existential in Bob’s choice, not universal.
Effect of $C$-vertices
At a $C$-vertex, Alice may choose to stop. This is critical:
- stopping avoids transitions
- therefore Bob cannot force continuation through that branch
To encode this correctly, we must treat $\bot$ as a successor that blocks derivation of $A^-$.
Thus at $C$-vertices, the rule remains unchanged:
$$ A^-(w) \Rightarrow A^-(v), $$
but since $\bot$ is never labeled $A^-$, Alice can always break a failed chain, and Bob’s forcing ability is correctly weakened.
No special clause is added; correctness comes from $\bot\notin A^-$.
7. Correct construction of $B^-(v)$
Symmetric:
If $v$ is marked $A$:
$$ \top \Rightarrow B^-(v). $$
If $v$ has no successors:
$$ \top \Rightarrow B^-(v). $$
For transitions:
$$ B^-(w) \Rightarrow B^-(v) \quad \text{for each } w \in \operatorname{Succ}(v). $$
Again $\bot$ is not in $B^-$, so accepting draw at $C$-vertices blocks forced propagation.
8. Why this correctly fixes the critical errors
8.1 Fixing the $A^-$, $B^-$ error
The previous solution incorrectly treated $A^-$ as a universal property:
$$ \bigwedge_{w} A^-(w) \Rightarrow A^-(v), $$
which assumes opponent control over all successors.
The corrected construction instead uses:
$$ A^-(w) \Rightarrow A^-(v), $$
which encodes existential control by the opponent.
This is the correct polarity: the opponent must be able to choose some safe continuation, not all.
Thus $A^-$ and $B^-$ are standard reachability-style inductive predicates in the dual game, not complements.
8.2 Fixing $C$-vertices
The previous error was ignoring the draw option.
Here it is modeled explicitly as a terminal successor $\bot$ that satisfies no predicate.
This ensures:
- players may stop at $C$-vertices,
- stopping blocks propagation of all four predicates,
- therefore it strictly reduces winning sets rather than incorrectly being ignored.
8.3 No acyclicity assumption
No reasoning about cycle elimination is used.
All four predicates are defined purely as least fixed points of monotone Horn systems over a finite graph extended with $\bot$.
Termination follows from finiteness of the Horn derivation process, not from strategy arguments.
9. Correctness statement
The Horn system computes the least fixed point of four monotone operators:
- $A^+$: Alice reachability of win states under existential choice
- $B^+$: Bob reachability of win states under existential choice
- $A^-$: Bob safety reachability avoiding Alice wins
- $B^-$: Alice safety reachability avoiding Bob wins
The $C$-vertex rule is enforced by adding a terminal successor $\bot$ that blocks all derivations.
Therefore:
- $A^+(v)$ is in the core iff Alice can force a win starting at $v$ moving first,
- $A^-(v)$ is in the core iff Bob can force that Alice cannot force a win,
- and symmetrically for $B^+$, $B^-$.
This exactly matches the game semantics.
Final conclusion
A correct Horn system exists only if:
- $A^-$ and $B^-$ are treated as inductive safety reachability predicates, not complements,
- $C$-vertices are modeled via an explicit terminal draw successor $\bot$,
- no acyclicity or strategy reduction assumptions are used.
This yields a fully monotone definite Horn construction consistent with the game rules.