this repo has no description
dekker.one
1% battleships.mzn.model
2% Ralph Becket <rafe@csse.unimelb.edu.au>
3% Wed Dec 10 13:51:12 EST 2008
4% vim: ft=zinc ts=4 sw=4 et tw=0
5%
6% A battleships puzzle involves working out where each of a fleet of ships
7% lies on a square grid. Clues are given in two ways: some parts of the
8% grid may be revealed as containing open water or part of a ship; and the
9% total number of parts of ships appearing in a row or column may also be
10% specified. Individual ships are always surrounded by open water, even
11% at the corners.
12%
13% The following example is taken from
14% http://wpc.puzzles.com/history/tests/1999qtest/test.htm
15%
16% w _ _ _ _ w _ _ _ 2 Fleet:
17% S w _ _ _ _ _ _ _ 2 1 battleship SSSS
18% _ _ _ _ _ _ _ _ _ 3 2 cruisers SSS SSS
19% w _ _ _ _ _ _ w _ 2 3 destroyers SS SS SS
20% _ _ _ _ _ _ _ _ _ 2 4 submarines S S S S
21% _ w S w _ _ _ _ _ 1
22% _ _ w _ _ _ _ S _ 5
23% _ _ _ _ _ _ _ _ _ 1
24% _ _ _ _ _ _ _ _ _ 2
25%
26% 4 0 3 2 2 2 1 4 2
27%
28% In this model, each square on the grid is a number from 0..4
29% (0 being water, 4 denoting the bows of a battleship). A Cruiser,
30% for instance, is described by a contiguous pattern 0 1 2 3 0 on
31% the board. Consider the following neighbourhood:
32%
33% a b c
34% d x e
35% f g h
36%
37% Precisely one of the following must hold:
38% - x is 0
39% - x is b + 1 and d = e = 0
40% - x is d + 1 and b = g = 0
41%
42% We also need to specify constraints on diagonally adjacent squares:
43% - if x < b then d = e = 0
44% - if x < d then b = g = 0
45%
46% The column (row) constraints specify how many non-zero elements a
47% column (row) must have.
48%
49% The fleet constraints specify how many instances of each positive number
50% must appear on the board.
51
52include "count.mzn";
53
54% Parameter: the length of side of the grid.
55%
56int: n;
57
58% Parameter: the number of ships of each class.
59%
60int: n_classes;
61set of int: class = 1..n_classes;
62array [class] of int: class_sizes;
63
64set of int: sq = {0} union class;
65
66% The row and column sums.
67%
68array [row] of var 0..n: row_sums;
69array [col] of var 0..n: col_sums;
70
71% We extend the board by one in each direction to add a sea border.
72%
73set of int: row = 1..n;
74set of int: col = 1..n;
75set of int: ROW = 0..(n + 1);
76set of int: COL = 0..(n + 1);
77array [ROW, COL] of var sq: a;
78
79% Add the sea border to the board.
80%
81constraint forall (r in {0, n + 1}, c in COL) (a[r, c] = 0);
82constraint forall (r in ROW, c in {0, n + 1}) (a[r, c] = 0);
83
84% Add the ship constraints.
85%
86constraint
87 forall (r in row, c in col) (
88 (
89 a[r, c] = 0
90 )
91 \/
92 (
93 a[r, c] = a[r, c - 1] + 1
94 /\ a[r - 1, c] = 0
95 /\ a[r + 1, c] = 0
96 )
97 \/
98 (
99 a[r, c] = a[r - 1, c] + 1
100 /\ a[r, c - 1] = 0
101 /\ a[r, c + 1] = 0
102 )
103 );
104
105% Add the diagonal constraints.
106%
107constraint
108 forall (r in row, c in col) (
109 (
110 a[r, c] < a[r, c - 1]
111 )
112 ->
113 (
114 a[r - 1, c] = 0
115 /\ a[r + 1, c] = 0
116 )
117 );
118
119constraint
120 forall (r in row, c in col) (
121 (
122 a[r, c] < a[r - 1, c]
123 )
124 ->
125 (
126 a[r, c - 1] = 0
127 /\ a[r, c + 1] = 0
128 )
129 );
130
131% Add the row and column constraints.
132%
133constraint
134 forall (r in row) (count([a[r, c] | c in col], 0, n - row_sums[r]));
135
136constraint
137 forall (c in col) (count([a[r, c] | r in row], 0, n - col_sums[c]));
138
139% Add the fleet constraints (a_flat is the 1D flattenning of the board, a).
140%
141array [1..(n * n)] of var sq: a_flat = [a[r, c] | r in row, c in col];
142
143constraint
144 forall (s in class) (
145 count(a_flat, s, sum (i in class where i >= s) (class_sizes[i]))
146 );
147
148solve
149 :: int_search(a_flat, first_fail, indomain_max, complete)
150 satisfy;
151
152output [ show(a[r, c]) ++ if c = n then "\n" else " " endif
153 | r in row, c in col
154 ];
155