this repo has no description
dekker.one
1/***
2!Test
3solvers: [gecode, chuffed]
4expected:
5- !Result
6 status: SATISFIED
7 solution: !Solution
8 s: !Range 1..9
9 t: !!set {45}
10 s_total: 45
11 t_total: 45
12- !Result
13 status: SATISFIED
14 solution: !Solution
15 s: !!set {100}
16 t: !!set {49, 51}
17 s_total: 100
18 t_total: 100
19- !Result
20 status: SATISFIED
21 solution: !Solution
22 s: !!set {1, 2, 40, 56, 94}
23 t: !!set {3, 93, 97}
24 s_total: 193
25 t_total: 193
26***/
27
28% Regression test for a bug in mzn2fzn 1.2. The optimisation pass was leaving
29% dangling references to variables it had "eliminated". The symptom was the
30% following error from the FlatZinc interpreter:
31%
32% subsets_100.fzn:413:
33% symbol error: `INT____407' undeclared
34%
35% (This model is from the original bug report.)
36
37% Subsets 100 puzzle in MiniZinc.
38%
39% From rec.puzzle FAQ
40% http://brainyplanet.com/index.php/Subsets?PHPSESSID=051ae1e2b6df794a5a08fc7b5ecf8028
41% """
42% Out of the set of integers 1,...,100 you are given ten different integers.
43% From this set, A, of ten integers you can always find two disjoint non-empty
44% subsets, S & T, such that the sum of elements in S equals the sum of elements
45% in T. Note: S union T need not be all ten elements of A. Prove this.
46% """
47
48%
49% This MiniZinc model was created by Hakan Kjellerstrand, hakank@bonetmail.com
50% See also my MiniZinc page: http://www.hakank.org/minizinc
51%
52
53% Note that this model is not run using CBC
54% This is because the solutions listed are not exhaustive, so we would usually check against another solver
55% However we cannot do this because when giving values for s or t then sum_set does not work
56% As the ub for the set will simply be the set itself, summing the wrong numbers
57
58include "globals.mzn";
59int: n = 100;
60int: m = 10;
61var set of 1..n: s;
62var set of 1..n: t;
63var int: s_total;
64var int: t_total;
65
66%
67% sums the integer in set ss
68%
69predicate sum_set(var set of int: ss, var int: total) =
70 let {
71 int: m = card(ub(ss)), % NOTE: This prevents checking of solutions since when fixing ss then card(ub(ss))=card(ss) so numbers are not summed correctly when checking
72 array[1..m] of var 0..1: tmp
73 }
74 in
75 forall(i in 1..m) (
76 i in ss <-> tmp[i] = 1
77 )
78 /\
79 total = sum(i in 1..m) (i*tmp[i])
80;
81
82
83solve :: set_search([s,t],
84 input_order, indomain_min, complete) satisfy;
85
86constraint
87 card(s union t) <= m
88 /\
89 card(s union t) > 0
90 /\
91 disjoint(s, t)
92 /\
93 sum_set(s, s_total)
94 /\
95 sum_set(t, t_total)
96 /\
97 s_total = t_total
98 % /\
99 % t_total = n
100;