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 117 118 119 120 121 122 123 124 125 126 127 128 | /* Maximum density still life in Comet. CSPLib 032: http://www.csplib.org/prob/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 This Comet model was created by Hakan Kjellerstrand (hakank@gmail.com) Also, see my Comet page: http://www.hakank.org/comet */ // Licenced under CC-BY-4.0 : http://creativecommons.org/licenses/by/4.0/ import cotfd; int t0 = System.getCPUTime(); int size = 6; // to change range objFunctionBoardCoord = 2..size+1; range checkConstraintsBoardCoord = 1..size+2; range augmentedBoardCoord = 0..size+3; Solver<CP> m(); // 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. var <CP>{ int } grid[augmentedBoardCoord,augmentedBoardCoord](m, 0..1); // Objective function: Maximize the number of live cells in the sub-board defined // by ignoring the first/last two/ rows/columns. Integer num_solutions(0); // exploreall<m> { maximize <m> sum (r in objFunctionBoardCoord, c in objFunctionBoardCoord) (grid[r,c]) subject to { // C1: Cells in the first/last two rows/columns are all 0 (dead) forall (x in augmentedBoardCoord) { m.post(grid[0,x] == 0); m.post(grid[1,x] == 0); m.post(grid[size+2,x] == 0); m.post(grid[size+3,x] == 0); m.post(grid[x,0] == 0); m.post(grid[x,1] == 0); m.post(grid[x,size+2] == 0); m.post(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. m.post(( ( 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) m.post((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 // m.post(grid[2,2] >= grid[size+1,size+1]); m.post(grid[2,size+1] >= grid[size+1,2]); } using { // labelFF(m); forall (i in augmentedBoardCoord, j in augmentedBoardCoord: !grid[i,j].bound()) { label(grid[i,j]); } num_solutions := num_solutions + 1; forall (i in augmentedBoardCoord) { forall (j in augmentedBoardCoord) { cout << grid[i,j] << " " ; } cout << endl; } cout << endl; } cout << "\nnum_solutions: " << num_solutions << endl; int t1 = System.getCPUTime(); cout << "time: " << (t1-t0) << endl; cout << "#choices = " << m.getNChoice() << endl; cout << "#fail = " << m.getNFail() << endl; cout << "#propag = " << m.getNPropag() << endl; |