this repo has no description
dekker.one
1/***
2!Test
3solvers: [gecode, chuffed]
4expected:
5- !Result
6 solution: !Solution
7 node_used: [3, 4, 6, 9, 11, 13, 15, 8, 9, 10, 11, 12, 13, 14, 15]
8 x: [6, 2, 6, 2, 4, 6, 8, 1, 2, 3, 4, 5, 6, 7, 8]
9***/
10
11% Regression test for a problem in mzn2fzn 1.2 where log/2
12% was not recognised as a built-in operation by the flattening
13% engine.
14
15% THe model is from: http://www.hakank.org/minizinc/decision_tree_binary.mzn
16
17% Decision tree in MiniZinc.
18%
19% Simple zero sum binary decision trees.
20%
21%
22% Model created by Hakan Kjellerstrand, hakank@bonetmail.com
23
24% The model only handles complete binary trees of sizes
25% n = (a**2) - 1, for some a. The values are at the lowest level.
26%
27% Example with n = 7
28%
29% x1 A maximizes
30% /\
31% x2 x3 B minimizes
32% / \ /\
33% x4 x5 x6 x7 (A)
34%
35% The value nodes (the last level):
36% x4 = 6
37% x5 = 1
38% x6 = 5
39% x7 = 3
40%
41% First B minimizes the last level (x4..x7):
42% x2 = argmin(x5, x4) -> x2 = x5
43% x3 = argmin(x6, x7) -> x3 = x7
44%
45% A then maximizes from B's choices as the last step:
46% x1 = argmax( x3, x2) -> x1 = x3
47%
48%
49% The solution is a decision tree represented here as as:
50%
51%
52% x (the values):
53% 3
54% 1 3
55% 6 1 5 3
56%
57% node_used:
58% 3
59% 5 7
60% 4 5 6 7
61
62
63%
64% minizinc and fz can handle n as large as 4095 (2**12-1)
65% without breaking much sweat.
66% For n = 8191 (2**13-1), it core dumps however.
67%
68
69
70int: n; % must be a (a**2) - 1, for some a, e.g. 7, 15, 31, 63 etc
71int: levels = n div 2; % the number of levels
72
73array[1..n] of var int: x; % the decision variables, the value tree
74array[1..n] of var 1..n: node_used; % the nodes indices
75
76
77%
78% tree_levels contains the levels in the tree, e.g.
79% [1, 2,2, 3,3,3,3, 4,4,4,4,4,4,4,4, ....]
80% for odd levels: A is trying to maximize his/her gain,
81% for even levels B is trying to minimize A's gains
82%
83array[1..n] of 0..n: tree_levels = [1+floor(log(2.0,int2float(i))) | i in 1..n ];
84
85% solve :: int_search(x, "first_fail", "indomain", "complete") satisfy;
86solve satisfy;
87
88%
89% argmax: maximize A's values
90%
91predicate argmax(array[int] of var int: x, int: i1, int: i2, array[int] of var int: node_used, int: node_used_ix) =
92 (x[i1] >= x[i2] -> node_used[node_used_ix] = i1)
93 /\
94 (x[i1] < x[i2] -> node_used[node_used_ix] = i2)
95;
96
97% argmin: minimize A's values
98predicate argmin(array[int] of var int: x, int: i1, int: i2, array[int] of var int: node_used, int: node_used_ix) =
99 (-x[i1] >= -x[i2] -> node_used[node_used_ix] = i1)
100 /\
101 (-x[i1] < -x[i2] -> node_used[node_used_ix] = i2)
102;
103
104predicate cp1d(array[int] of var int: x, array[int] of var int: y) =
105 assert(index_set(x) = index_set(y),
106 "cp1d: x and y have different sizes",
107 forall(i in index_set(x)) ( x[i] = y[i] ) )
108;
109
110
111constraint
112
113 % the first 1..n div 2 in x is to be decided by the model,
114 % the rest is the node values.
115
116 cp1d(x, [_, _,_, _,_, _,_, 1,2, 3,4, 5,6, 7,8]) % n = 15
117
118 /\ % the last n div 2 positions (the node "row") in node_used is static
119 forall(i in levels+1..n) (
120 node_used[i] = i
121 % more general: makes the node value 1.. .
122 % Comment it if another tree should be used.
123 % /\ x[i] = -(n - i - levels) + 1
124 )
125 /\
126 % the first n div 2 positions and values are dynamic,
127 % the rest are static.
128 forall(i in 1..levels) (
129 x[i] = x[node_used[i]]
130 )
131 /\ % Should we maximize or minimize?
132 % It depends on the level.
133 forall(i in 1..levels) (
134 if tree_levels[i] mod 2 = 1 then
135 argmax(x, 2*i, 2*i+1, node_used, i)
136 else
137 argmin(x, 2*i, 2*i+1, node_used, i)
138 endif
139 )
140
141;
142
143% A "nice tree" (OK, it's not so nice. :-)
144output
145["x (the values):\n" , show(x[1])]
146++
147[
148 if tree_levels[i] > tree_levels[i-1] then "\n" else " " endif ++
149 show(x[i])
150 | i in 2..n
151] ++
152["\n\nnode_used:\n", show(node_used[1])]
153++
154[
155 if tree_levels[i] > tree_levels[i-1] then "\n" else " " endif ++
156 show(node_used[i])
157 | i in 2..n
158] ++ ["\n"];
159
160n = 15;