1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 | % % Maximum density still life in MiniZinc. % % % CSPLib 032: http://www.csplib.org/Problems/prob032 % % % This model was inspired by the OPL model from % Toni Mancini, Davide Micaletto, Fabio Patrizi, Marco Cadoli: % "Evaluating ASP and commercial solvers on the CSPLib" % http://www.dis.uniroma1.it/~tmancini/index.php?problemid=032&solver=OPL&spec=BASE&currItem=research.publications.webappendices.csplib2x.problemDetails#listing % % % Compare with the Comet model: % % % This MiniZinc model was created by Hakan Kjellerstrand, hakank@gmail.com % See also my MiniZinc page: http://www.hakank.org/minizinc % % Licenced under CC-BY-4.0 : http://creativecommons.org/licenses/by/4.0/ % include "globals.mzn"; int : size = 7; % to change set of int : objFunctionBoardCoord = 2.. size +1; set of int : checkConstraintsBoardCoord = 1.. size +2; set of int : augmentedBoardCoord = 0.. size +3; % Search space: The set of all possible assignments of 0s (dead) and 1s (live) % to the cells of the board section. However, to be able to easily express % constraints on "boundary" cells, we take as search space the set of 0/1 % boards of size n+4 by n+4: the actual stable pattern appears in the sub-board % defined by ignoring the first/last two rows/columns. array [augmentedBoardCoord,augmentedBoardCoord] of var 0..1: grid; var int : z = sum (r in objFunctionBoardCoord, c in objFunctionBoardCoord) (grid[r,c]); % Objective function: Maximize the number of live cells in the sub-board defined % by ignoring the first/last two/ rows/columns. % solve maximize z; solve :: int_search( [grid[i,j] | i,j in augmentedBoardCoord], smallest, indomain_max, complete) maximize z; constraint % C1: Cells in the first/last two rows/columns are all 0 (dead) forall (x in augmentedBoardCoord) ( grid[0,x] = 0 /\ grid[1,x] = 0 /\ grid[ size +2,x] = 0 /\ grid[ size +3,x] = 0 /\ grid[x,0] == 0 /\ grid[x,1] == 0 /\ grid[x, size +2] = 0 /\ grid[x, size +3] = 0 ) /\ forall (r in checkConstraintsBoardCoord,c in checkConstraintsBoardCoord) ( % C2: Each cell of the board (except those of the first/last row/column) % that has exactly three live neighbors is alive. % Together with constraint C1, this implies that cells in the % second/last-but-one row/column cannot have three live neighbors. ( ( ( grid[r-1,c-1] + grid[r-1,c] + grid[r-1,c+1] + grid[r,c-1] + grid[r,c+1] + grid[r+1,c-1] + grid[r+1,c] + grid[r+1,c+1] ) = 3 ) -> (grid[r,c] = 1) ) /\ % C3: Each live cell must have 2 or 3 live neighbors (cells of the first/last % row/column may be ignored by this constraint) ( (grid[r,c] = 1) -> ( 2 <= ( grid[r-1,c-1] + grid[r-1,c] + grid[r-1,c+1] + grid[r,c-1] + grid[r,c+1] + grid[r+1,c-1] + grid[r+1,c] + grid[r+1,c+1] ) /\ ( grid[r-1,c-1] + grid[r-1,c] + grid[r-1,c+1] + grid[r,c-1] + grid[r,c+1] + grid[r+1,c-1] + grid[r+1,c] + grid[r+1,c+1] ) <= 3 ) ) ) /\ % SBSO: Symmetry-breaking by selective ordering % The assignment is forced to respect an ordering on the values that occur in corner entries % of the board. In particular: % - if the NW-corner cell is dead, the SE-corner cell % must be dead too % - if the NE-corner cell is dead, the SW-corner cell must be dead too % grid[2,2] >= grid[ size +1, size +1] /\ grid[2, size +1] >= grid[ size +1,2] ; output [ if j = 0 then "\n" else " " endif ++ show (grid[i,j]) | i,j in augmentedBoardCoord ]; |