A set of benchmarks to compare a new prototype MiniZinc implementation
dekker.one
1%------------------------------------------------------------------------------%
2
3include "count.mzn";
4
5%------------------------------------------------------------------------------%
6% Parameters
7
8int: X; % Number of cells in the x-direction
9int: Y; % NUmber of cells in the y-direction
10int: N; % Number of pairs
11
12set of int: Pairs = 1..N;
13set of int: Xs = 1..X;
14set of int: Ys = 1..Y;
15
16 % These arrays all correspond.
17 %
18array[Pairs] of Xs: end_points_start_x;
19array[Pairs] of Ys: end_points_start_y;
20array[Pairs] of Xs: end_points_end_x;
21array[Pairs] of Ys: end_points_end_y;
22
23set of int: Dom = 0..N;
24
25%------------------------------------------------------------------------------%
26% Variables
27
28array [Xs, Ys] of var Dom: board;
29array[int] of var Dom: board_check = array1d(board);
30
31%------------------------------------------------------------------------------%
32% Tests
33
34test is_end_point(int: x, int: y) =
35 exists(i in Pairs)(
36 (end_points_start_x[i] = x /\ end_points_start_y[i] = y)
37 \/ (end_points_end_x [i] = x /\ end_points_end_y [i] = y)
38 );
39
40test is_neighbour_from_xy(int: x, int: y, int: u, int: v) = (
41 u in Xs /\ v in Ys /\ x in Xs /\ y in Ys
42/\ ( (x == u /\ y in {v - 1, v + 1})
43 \/ (y == v /\ x in {u - 1, u + 1})
44 )
45);
46
47%------------------------------------------------------------------------------%
48% Constraints
49
50 % Endpoints must be match with input
51 %
52constraint
53 forall(i in Pairs)(
54 board[end_points_start_x[i], end_points_start_y[i]] = i
55 /\ board[end_points_end_x [i], end_points_end_y [i]] = i
56 );
57
58 % Every endpoint has exactly one neighbour
59 %
60constraint
61 forall(i in Pairs)(
62 let {
63 int: x1 = end_points_start_x[i],
64 int: y1 = end_points_start_y[i],
65 int: y2 = end_points_end_y [i],
66 int: x2 = end_points_end_x [i]
67 } in (
68 count([board[u, v] | u in x1-1..x1+1, v in y1-1..y1+1 where
69 is_neighbour_from_xy(x1, y1, u, v)], i, 1
70 )
71 /\ count([board[u, v] | u in x2-1..x2+1, v in y2-1..y2+1 where
72 is_neighbour_from_xy(x2, y2, u, v)], i, 1
73 )
74 )
75 );
76
77 % Interior points has exactly two neighbours
78 %
79constraint
80 forall(x in Xs, y in Ys)(
81 if is_end_point(x, y) then
82 true
83 else
84 board[x, y] != 0 ->
85 count([board[u, v] | u in x-1..x+1, v in y-1..y+1 where
86 is_neighbour_from_xy(x, y, u, v)], board[x, y], 2)
87 endif
88 );
89
90 % Some redudant constraints
91 %
92constraint redundant_constraint(
93 forall(i in Pairs)(
94 let {
95 int: x1 = min(end_points_start_x[i], end_points_end_x[i]),
96 int: y1 = min(end_points_start_y[i], end_points_end_y[i]),
97 int: x2 = max(end_points_start_x[i], end_points_end_x[i]),
98 int: y2 = max(end_points_start_y[i], end_points_end_y[i])
99 } in (
100 if x1 + 1 < x2 then
101 forall(x in x1+1..x2-1)(
102 sum(z in Ys)(bool2int(board[x, z] == i)) > 0
103 )
104 else
105 true
106 endif
107 /\ if y1 + 1 < y2 then
108 forall(y in y1+1..y2-1)(
109 sum(z in Xs)(bool2int(board[z, y] == i)) > 0
110 )
111 else
112 true
113 endif
114 )
115 )
116);
117
118%------------------------------------------------------------------------------%
119% Search
120
121solve
122 :: int_search(array1d(1..X*Y, board), input_order, indomain_split, complete)
123 satisfy;
124
125%------------------------------------------------------------------------------%
126% Output
127
128output [
129 "% "
130] ++ [
131 show_int(floor(log10(int2float(N)) + 1.0), board[x, y]) ++
132 if x = X then "\n% " else " " endif
133| y in Ys, x in Xs
134] ++ [
135 "\nboard = array2d(", show(Xs), ", ", show(Ys), ", ", show(board), ");\n"
136];
137