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