Download
language ESSENCE' 1.0
$ ---- Parameters & Constants ----
$ **** Allowing 0 here for testing purposes only
given initGrid : matrix indexed by[int(1..gridHeight), int(1..gridWidth)] of int(0..)
letting GRIDCOLS be domain int(1..gridWidth)
letting GRIDROWS be domain int(1..gridHeight)
letting NOBLOCKS be gridWidth * gridHeight
letting COLOURS be domain int(1..max(flatten(initGrid)))
letting EMPTY be 0
letting EMPTYANDCOLOURS be domain int(EMPTY) union COLOURS
given goalBlocksRemaining : int(0..NOBLOCKS)
given noSteps : int(1..)
letting STEPSFROM1 be domain int(1..noSteps)
letting STEPSFROM0 be domain int(0..noSteps)
$ ---- Decision Variables ----
$ NB Actual game sometimes restricted firing positions.
find fpRow : matrix indexed by[STEPSFROM1] of int(0..gridHeight)
find fpCol : matrix indexed by[STEPSFROM1] of int(0..gridWidth)
find grid : matrix indexed by[STEPSFROM0, GRIDROWS, GRIDCOLS]
of EMPTYANDCOLOURS
find hand : matrix indexed by[STEPSFROM0] of COLOURS
$ Aux to deal with shot down a row hitting a wall and then falling.
find wallFall : matrix indexed by[STEPSFROM1] of int(0..gridHeight)
$ Aux to deal with monochrome column symmetry
$ 0 means empty or non-monochrome.
find monochromeCols : matrix indexed by[STEPSFROM0, GRIDCOLS] of EMPTYANDCOLOURS
$ ---- Constraints -------------------------------------------------------------
such that
$ ---- Initial & Goal States ----------------------------
$ Initial state:
forAll gCol : GRIDCOLS .
forAll gRow : GRIDROWS .
grid[0, gRow, gCol] = initGrid[gRow, gCol],
$ Goal state:
atleast(flatten(grid[noSteps,..,..]),
[NOBLOCKS - goalBlocksRemaining],
[EMPTY]),
$ ---- End of Initial & Goal States ---------------------
$ ---- Constrain Actions --------------------------------
$ Each move must do something useful:
$ Careful: if not counting 0s then it will try and insert phantom colours.
forAll step : STEPSFROM1 .
sum(flatten(grid[step-1,..,..])) > sum(flatten(grid[step,..,..])),
$ Exactly one fp axis must be 0. (exclusive OR, only ONE fired angle)
forAll step : STEPSFROM1 .
(
(fpRow[step] * fpCol[step]) = 0 /\ (fpRow[step] + fpCol[step]) > 0
),
$ ---- End of Constrain Actions -------------------------
$ ---- Implied Constraint ------------------------------------------------------
$ If there is only cell of a particular colour left in the grid then it cannot
$ appear in the hand before the goal state.
forAll step : int(0..noSteps-2) .
forAll colour : COLOURS .
atmost(flatten(grid[step,..,..]), [1], [colour])
->
forAll step2 : int(step+1..noSteps-1) .
hand[step2] != colour,
$ ---- Compute wallFall distance-----------------------
$ The number of blocks travelled in the final column by the shot block.
$ Checks at least one block consumed en route to force progressing move.
$ 0 if no travel in final col.
forAll step : STEPSFROM1 .
forAll i : int (1..gridHeight) .
(wallFall[step] = i)
=
(exists row : int(1..gridHeight) .
(fpRow[step] = row) /\
$ Travelled to the rightmost column
(forAll col : int(1..gridWidth) .
grid[step-1,row,col] = EMPTY \/
grid[step-1,row,col] = hand[step-1]) /\
$ Travelled i in the last column
(forAll underRow : int (row..row+i-1) .
grid[step-1,underRow,gridWidth] = hand[step-1] \/
grid[step-1,underRow,gridWidth] = EMPTY) /\
$ And no more
((grid[step-1,row+i,gridWidth] != hand[step-1]) \/
(row+i > gridHeight)) /\
$ And consumed a block somewhere, otherwise not a progressing move.
((exists col : GRIDCOLS .
grid[step-1,row,col] = hand[step-1]) \/
(exists underRow : int(row..row+i-1) .
grid[step-1,underRow,gridWidth] = hand[step-1]))
),
$ ---- End of Compute wallFall distance----------------
$ ---- The hand stays the same ------------------------
$ There are only two cases when we require a progressing move.
$ Otherwise the hand must change.
forAll step : STEPSFROM1 .
(hand[step-1] = hand[step])
=
(
$ Fired down col, hitting wall
(
(forAll colBlock : GRIDROWS .
((grid[step-1,colBlock,fpCol[step]] = hand[step-1]) \/
(grid[step-1,colBlock,fpCol[step]] = EMPTY))
)
) \/
$ Fired row, hitting wall, dropping through hand-colour only.
$ We can test this by comparing the wallFall value with fpRow:
(wallFall[step] = gridHeight-fpRow[step]+1)
),
$ ---- End of The hand stays the same -----------------
$ ---- Emptiness --------------------------------------
$ If a cell is empty then one of these cases must apply, and conversely.
forAll step : STEPSFROM1 .
forAll gRow : GRIDROWS .
forAll gCol : GRIDCOLS .
(grid[step,gRow,gCol] = EMPTY)
=
(
$ When a cell is EMPTY, it stays EMPTY
(grid[step-1,gRow,gCol] = EMPTY) \/
$ Deleted by shot down column
(
$ The right column
(fpCol[step] = gCol) /\
$ same colour as hand
(grid[step-1,gRow,gCol] = hand[step-1]) /\
$ Nothing blocking the way
(forAll blockAbove : int(1..gRow-1) .
((grid[step-1,blockAbove,fpCol[step]] = hand[step-1]) \/
(grid[step-1,blockAbove,fpCol[step]] = EMPTY))
)
) \/
$ Deleted by shot along row. Doesn't include last column.
(
$ The right row
(fpRow[step] = gRow) /\
$ Interior column.
(gCol < gridWidth) /\
$ same colour as hand
(grid[step-1,gRow,gCol] = hand[step-1]) /\
$ no block above. This is why not last col: can't check 1 block above.
((gRow = 1) \/
(grid[step-1,gRow-1,gCol] = EMPTY)) /\
$ nothing blocking way
(forAll blockLeft : int(1..gCol-1) .
((grid[step-1,gRow,blockLeft] = hand[step-1]) \/
(grid[step-1,gRow,blockLeft] = EMPTY))
)
) \/
$ Deleted by shot along row, then down col
(
$ Only the final column
(gCol = gridWidth) /\
$ Can exploit wallfall here: fpRow..fpRow+WF-1 is directly deleted
(gRow >= fpRow[step]) /\
(gRow <= fpRow[step]+wallFall[step]-1) /\
$ Now check there was nothing there
(
(gRow - wallFall[step] < 1) \/
(grid[step-1,gRow - wallFall[step], gridWidth] = EMPTY)
)
) \/
$ Fall from this cell to become empty: row shot underneath, not last col.
(
$ There was no block above
((grid[step-1,gRow-1,gCol] = EMPTY) \/
(gRow = 1)) /\
$ Interior column.
(gCol < gridWidth) /\
$ Deletion below
(fpRow[step] > gRow) /\
(forAll delBlock : int(1..gCol) .
((grid[step-1,fpRow[step],delBlock] = hand[step-1]) \/
(grid[step-1,fpRow[step],delBlock] = EMPTY)))
) \/
$ Final Column shot along a row consuming several blocks underneath
(
$ Only the final column
(gCol = gridWidth) /\
$ There was a wallfall - this implies a successful row shot.
(wallFall[step] > 0) /\
$ The shot was beneath here
(fpRow[step] > gRow) /\
$ Nothing there to fall into here
(grid[step-1,gRow-wallFall[step],gridWidth] = EMPTY \/
gRow-wallFall[step] < 1)
)
),
$ ---- End of Emptiness -------------------------------
$ ---- Grid Stays Same --------------------------------
$ A cell stays the same if one of these cases applies.
forAll step : STEPSFROM1 .
forAll gRow : GRIDROWS .
forAll gCol : GRIDCOLS .
(grid[step,gRow,gCol] = grid[step-1,gRow,gCol])
=
(
$ It was empty
(grid[step-1,gRow,gCol] = EMPTY) \/
$ Fired beneath this row, not far enough to cause fall:
(
(fpRow[step] > gRow) /\
(exists blockLeft : int(1..gCol) .
((grid[step-1,fpRow[step],blockLeft] != EMPTY) /\
(grid[step-1,fpRow[step],blockLeft] != hand[step-1]))
)
) \/
$ Fired along this row, but something in the way
(
(fpRow[step] = gRow) /\
(exists blockLeft : int(1..gCol-1) .
((grid[step-1, gRow, blockLeft] != EMPTY) /\
(grid[step-1, gRow, blockLeft] != hand[step-1]))
)
) \/
$ Fired along row above, cols except last
(
(gCol < gridWidth) /\
(fpRow[step] != 0) /\
(fpRow[step] < gRow)
) \/
$ Fired along row above, last col. Sth in way on row or last col.
(
(gCol = gridWidth) /\
(fpRow[step] != 0) /\
(fpRow[step] < gRow) /\
(
(exists rowBlock : int(1..gridWidth) .
((grid[step-1, fpRow[step], rowBlock] != EMPTY) /\
(grid[step-1, fpRow[step], rowBlock] != hand[step-1]))
) \/
(exists colBlock : int(1..gRow-1) .
((colBlock >= fpRow[step]) /\
(grid[step-1, colBlock, gridWidth] != EMPTY) /\
(grid[step-1, colBlock, gridWidth] != hand[step-1]))
)
)
) \/
$ Fired down this column, but something in way
(
(fpCol[step] = gCol) /\
(exists blockAbove : int(1..gRow-1) .
((grid[step-1,blockAbove,gCol] != EMPTY) /\
(grid[step-1,blockAbove,gCol] != hand[step-1])))
) \/
$ Fired down a different column
(
(fpCol[step] != 0) /\
(fpCol[step] != gCol)
) \/
$ This row or below. Same colour block falls here. All but last col.
(
(gCol < gridWidth) /\
(fpRow[step] >= gRow) /\
(forAll delBlock : int(1..gCol) .
((grid[step-1,fpRow[step],delBlock] = hand[step-1]) \/
(grid[step-1,fpRow[step],delBlock] = EMPTY))) /\
(grid[step-1,gRow-1,gCol] = grid[step-1,gRow,gCol])
) \/
$ This row or below. Same colour block falls here. Last col.
(
(gCol = gridWidth) /\
(fpRow[step] >= gRow) /\
(wallFall[step] > 0) /\
(grid[step-1,gRow-wallFall[step],gCol] = grid[step-1,gRow,gCol])
)
),
$ ---- End of Grid Stays Same -------------------------
$ ---- Grid changes to something other than empty -----
forAll step : STEPSFROM1 .
forAll gRow : GRIDROWS .
forAll gCol : GRIDCOLS .
$ makeTable around this runs forever (search not table making)
((grid[step,gRow,gCol] != grid[step-1,gRow,gCol]) /\
(grid[step,gRow,gCol] != EMPTY))
=
(
$ Fall from above. Not rightmost col.
(
(gCol < gridWidth) /\
$there was a block above
(grid[step-1,gRow-1,gCol] != EMPTY) /\
$Deletion here or below
(fpRow[step] >= gRow) /\
(forAll delBlock : int(1..gCol) .
((grid[step-1,fpRow[step],delBlock] = hand[step-1]) \/
(grid[step-1,fpRow[step],delBlock] = EMPTY))) /\
$ Is now the same as the block above.
(grid[step,gRow,gCol] = grid[step-1,gRow-1,gCol]) /\
$ Which was a different colour
(grid[step-1,gRow,gCol] != grid[step-1,gRow-1,gCol])
) \/
$ Fall from above. Rightmost col.
(
(gCol = gridWidth) /\
$ WallFall implies successful row shot
(wallFall[step] > 0) /\
$ It's in the wall fall area. Everything down to fprow+wallfall-1 changes
(gRow <= fpRow[step] + wallFall[step] - 1) /\
$ Is now the same as the block above
(grid[step,gRow,gridWidth] =
grid[step-1,gRow-wallFall[step],gridWidth]) /\
$ Which was a different colour, and not empty.
(grid[step-1,gRow,gridWidth] !=
grid[step-1,gRow-wallFall[step],gridWidth]) /\
(grid[step-1,gRow-wallFall[step],gridWidth] != EMPTY)
) \/
$ Cell swaps with hand: row shot.
(
(gRow = fpRow[step]) /\
$ The row shot
(forAll colsLeft : int(1..gCol-1) .
(grid[step-1,fpRow[step],colsLeft] = hand[step-1]) \/
(grid[step-1,fpRow[step],colsLeft] = EMPTY)) /\
$ At least one cell has to match the hand
(exists colsLeft : int(1..gCol-1) .
(grid[step-1,fpRow[step],colsLeft] = hand[step-1])) /\
$ Exchanges with the hand
(hand[step] = grid[step-1,fpRow[step],gCol]) /\
(hand[step-1] = grid[step,fpRow[step],gCol]) /\
$ Which was a different colour
(hand[step-1] != grid[step-1,fpRow[step],gCol])
) \/
$ Cell swaps with hand: col shot
(
(gCol = fpCol[step]) /\
$ The col shot
(forAll rowsAbove : int(1..gRow-1) .
(grid[step-1,rowsAbove,fpCol[step]] = hand[step-1]) \/
(grid[step-1,rowsAbove,fpCol[step]] = EMPTY)) /\
$ At least one cell has to match the hand
(exists rowsAbove : int(1..gRow-1) .
(grid[step-1,rowsAbove,fpCol[step]] = hand[step-1])) /\
$ Exchanges with the hand
(hand[step] = grid[step-1,gRow,fpCol[step]]) /\
(hand[step-1] = grid[step,gRow,fpCol[step]]) /\
$ Which was a different colour
(hand[step-1] != grid[step-1,gRow,fpCol[step]])
) \/
$ Cell swaps with hand: row then down last col.
(
$ rightmost col
(gCol = gridWidth) /\
$ WallFall implies travel row then col.
(wallFall[step] > 0) /\
$ and this cell must be at fpRow+wallFall
(gRow = wallFall[step] + fpRow[step]) /\
$ Some consumption must have happened in either row or col.
$ Exchanges with hand
(hand[step] = grid[step-1,gRow,gridWidth]) /\
(hand[step-1] = grid[step,gRow,gridWidth]) /\
$ Which was a different colour
(hand[step-1] != grid[step-1,gRow,gridWidth])
)
),
$ ---- End: Grid changes to something other than empty
$ ---- Interchangeable Moves
$ Sequences of monochrome column shots can be permuted. Break that sym.
$ Channel to the monochrome columns variables.
$ Set up an iff for each colour, defaults to 0 for empty or non-monochrome.
forAll step : int(0..noSteps) .
forAll gCol : int(1..gridWidth) .
forAll colour : COLOURS .
(monochromeCols[step, gCol] = colour)
=
(
$ not empty
(grid[step, gridHeight, gCol] = colour) /\
$ monochrome
(forAll gRow : int(1..gridHeight-1) .
(grid[step, gRow, gCol] = colour) \/
(grid[step, gRow, gCol] = EMPTY))
),
$ Use monochrome columns variables to break the symmetry.
forAll step : int(1..noSteps-1) .
forAll gCol : int(1..gridWidth-1) .
forAll gCol2 : int(gCol+1..gridWidth) .
((monochromeCols[step-1, gCol] != EMPTY) /\
(monochromeCols[step-1, gCol] = monochromeCols[step-1, gCol2]))
->
(
$ If consecutive must be left to right
fpCol[step] = gCol2
->
fpCol[step+1] != gCol
),
$ ---- End of Interchangeable Moves
true