For Chomp, one representation is a Boolean array
occupied(y)(x) with one entry per cell. The initial board has every entry true. For the noninitial board in the figure, the sets of occupied column indices in successive rows are , , , , , ; all other entries are false.A more compact representation is the monotone boundary representation of a grid order ideal: an array
row(y) giving the number of occupied cells in row . Occupied cells in a row always form a left prefix. The initial representation is , and the illustrated noninitial representation is , indexed upwards from row zero. Its total is . These descriptions use the same coordinate orientation as the original figure; no source image is needed in the solution.Let the abstract state be the set of occupied coordinate pairs. For the Boolean array, the abstraction function is . Its representation invariant requires an Boolean array and the downward-closure propertyThus 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 areThe array has length . Removing at replaces each
row(j) for by . Earlier rows are unchanged. This both implements the abstract removal and preserves the nonincreasing boundary.Without a cached count, the Boolean representation takes for
Count, for Legal, worst-case for Move, and for a full-grid Display. The boundary representation takes for Count, for Legal, worst-case for Move, and for the same full-grid Display. Their space complexities are respectively and . A scalar cached total makes Count in either representation if each move updates it consistently. The implementation below uses that cache with the boundary array, so it achieves 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.Use the row boundary and cache its sum. The restriction on the initial total makes the fixed The additional representation invariant is . It initially holds. For
Int return type of Count meaningful; Display separately checks the requested single-digit coordinate range.class Chomps(N: Int) {
require(N > 0 && N.toLong * N.toLong <= Int.MaxValue.toLong)
private val row = Array.fill(N)(N)
private var remaining = N * N
def Count(): Int = remaining
def Legal(x: Int, y: Int): Boolean =
0 <= x && x < N && 0 <= y && y < N && x < row(y)
def Move(x: Int, y: Int): Unit = {
require(Legal(x, y))
var j = y
while (j < N) {
val next = math.min(row(j), x)
remaining -= row(j) - next
row(j) = next
j += 1
}
}
def Display(): Unit = {
require(N < 10)
var y = N - 1
while (y >= 0) {
print(y.toString + " ")
var x = 0
while (x < N) {
print(if (x < row(y)) "* " else " ")
x += 1
}
println()
y -= 1
}
print(" ")
var x = 0
while (x < N) {
print(x.toString + " ")
x += 1
}
println()
}
}Move, write for the boundary at entry. The loop invariant says that rows before are unchanged, rows from through equal , rows from onwards still equal , and remaining equals the sum of the current entries. The loop variant is . Each iteration subtracts exactly the newly removed number of cells from the cache. At exit all affected rows are truncated as required, and the nonincreasing boundary is restored. During a partially completed update it need not be nonincreasing; only the stated loop invariant, not the full externally visible representation invariant, is required internally.For
Display, the outer loop invariant says that exactly the rows with indices greater than have been printed correctly; its loop variant is . The inner loop invariant says that the current row's first cells have been emitted correctly; its loop variant is . The final labels loop has the same decreasing loop variant, and prints exactly the first column labels before each iteration. Short-circuit evaluation in Legal checks both coordinates before indexing. An illegal Move fails before changing the board.Keep the same player until an occupied, in-range cell is supplied:The outer loop invariant is that
val board = new Chomps(6)
var player = 1
while (board.Count() > 0) {
board.Display()
var x = -1
var y = -1
while (!board.Legal(x, y)) {
println("Player " + player + ": enter x, then y")
try {
x = scala.io.StdIn.readInt()
y = scala.io.StdIn.readInt()
} catch {
case _: NumberFormatException =>
x = -1
y = -1
}
if (!board.Legal(x, y)) println("Choose an occupied cell")
}
board.Move(x, y)
if (board.Count() == 0)
println("Player " + player + " loses; player " + (3 - player) + " wins")
else player = 3 - player
}player is the next player's number, either one or two, and the board is the result of the accepted moves. The inner loop invariant says that the board and player have not changed; rejected inputs do not consume a turn. Assuming the input source continues and eventually supplies a legal coordinate pair, the inner loop finishes. No program can guarantee that a user stops entering illegal moves, so that interaction assumption is necessary.Every accepted move removes at least its selected token, so the outer loop variant is
Count(), a decreasing nonnegative integer. In a nonempty order ideal, is occupied. Removing it removes the entire board, whereas a move at any other cell leaves it. Therefore the player making the final move is exactly the loser; the code reports that player before changing the turn. At most legal moves occur. Articles by others on the same topic
There are currently no matching articles.