= Solution
Let the abstract state be the <set> $B$ of occupied coordinate pairs. For the Boolean <array>, the <abstraction function> is $\alpha(occupied)=\{(x,y):occupied(y)(x)\}$. Its <representation invariant> requires an $N\times N$ Boolean <array> and the downward-closure property
$$
(x,y)\in B\ \Longrightarrow\ (i,j)\in B
\quad\text{whenever }0\leq i\leq x,\ 0\leq j\leq y.
$$
Thus $B$ is an <order ideal> for the coordinatewise <partial order>. Removing an upper-right rectangle preserves this property. The empty <set> is allowed after the losing move.
For the row-boundary <array>, the <abstraction function> and <representation invariant> are
$$
\alpha(row)=\{(x,y):0\leq y<N,\ 0\leq x<row(y)\},
\qquad N\geq row(0)\geq\cdots\geq row(N-1)\geq0.
$$
The <array> has length $N$. Removing at $(x,y)$ replaces each `row(j)` for $j\geq y$ by $\min(row(j),x)$. Earlier rows are unchanged. This both implements the abstract removal and preserves the nonincreasing boundary.
Without a cached count, the Boolean representation takes $\Theta(N^2)$ for `Count`, $O(1)$ for `Legal`, $O(N^2)$ worst-case for `Move`, and $\Theta(N^2)$ for a full-grid `Display`. The boundary representation takes $\Theta(N)$ for `Count`, $O(1)$ for `Legal`, $O(N)$ worst-case for `Move`, and $\Theta(N^2)$ for the same full-grid `Display`. Their <space complexities> are respectively $\Theta(N^2)$ and $\Theta(N)$. A scalar cached total makes `Count` $O(1)$ in either representation if each move updates it consistently. The implementation below uses that cache with the boundary <array>, so it achieves \b[constant-time `Count` and `Legal`, linear worst-case `Move`, and linear storage]. Full-grid output still takes quadratic time because it emits quadratic many cell positions.
Back to article page
