Download
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.
 
 
 
  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;