Download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
%
% Water buckets problem in Minizinc
%
% Inpiration from the OPL code at
% http://www.dis.uniroma1.it/~tmancini/index.php?currItem=research.publications.webappendices.csplib2x.problemDetails&problemid=018
 
% """
% Problem description
% This is a generalization of the CSPLib specification, which is as follows: Given an 8 pint bucket of water, and two empty buckets which can contain 5 and 3 pints respectively, the problem requires to divide the water into two by pouring water between buckets (that is, to end up with 4 pints in the 8 pint bucket, and 4 pints in the 5 pint bucket) in the smallest number of transfers.
%
% The generalization consists in making the specification parametric with respect to the start and goal configurations, which are now inputs to the problem.
%
% Problem input
%
% * Function start, assigning an initial amount of water to each bucket
% * Function goal, assigning the goal amount of water to each bucket
%
% Search space
% The set of all possibile sequences of configurations (states), where a configuration is a triple encoding the amount of water in each bucket at a given time-step
%
% Constraints
%
% * C1: At beginning, buckets contain the amount of water specified by function start
% * C2: At the end, buckets contain the amount of water specified by function goal
% * C3: The configuration at each step differs from that of the next one in that the amount of water of exactly 2 buckets changes (that in the others remain the same)
% * C4: The overall amount of water is the same at each time step
% * C5: After each transition (involving buckets b1 and b2), either the source bucket becomes empty, or the target becomes full
% """
%
% Model created by Hakan Kjellerstrand, hakank@gmail.com
% See also my MiniZinc page: http://www.hakank.org/minizinc/
%
 
% Licenced under CC-BY-4.0 : http://creativecommons.org/licenses/by/4.0/
 
int: nb_buckets = 3;
int: max_step = 10; % 8 for satisfy
set of int: buckets = 1..nb_buckets;
set of int: steps = 1..max_step;
array[buckets] of int: capacity = [8,5,3];
array[buckets] of int: start = [8,0,0];
array[buckets] of int: goal = [4,4,0];
 
% Search space: The set of all possibile sequences of configurations (states),
% where a configuration is a triple encoding the amount of water in each
% bucket at a given time-step
array[steps, buckets] of var int: state;
var 1..max_step: goal_step;
 
% Objective function
solve minimize goal_step;
% solve :: int_search( [ state[i,j] | i in steps, j in buckets ] , "first_fail", "indomain", "complete")  minimize goal_step;
 
constraint
%   goal_step <= 8 % for solve satisfy
%   /\
   % assertions
   forall(b in buckets) (
      (start[b] <= capacity[b]) /\ (goal[b] <= capacity[b])
   )
   /\
   sum(b in buckets)(start[b]) = sum(b in buckets)(goal[b])
   /\
   forall(s in steps, b in buckets) (
      state[s,b] >= 0 /\
      state[s,b] <= capacity[b]
   )
   /\
   forall(b in buckets) (
      % C1: At beginning, buckets contain the amount of water specified by function start
      state[1,b]=start[b]
      /\
      % C2: At the end, buckets contain the amount of water specified by function goal
      state[goal_step,b] = goal[b]
   )
   /\
   forall(step in 1..max_step-1) (
      % C3: The configuration at each step differs from that of the next one in that the amount of
      % water of exactly 2 buckets changes (that in the others remain the same)
      sum(b in buckets)( bool2int(state[step,b] != state[step+1, b])) = 2
      /\
      % C4: The overall amount of water is the same at each time step
      sum(b in buckets)(state[step,b]) = sum(b in buckets)(state[step+1,b])
      /\
 
      % C5: After each transition (involving buckets b1 and b2), either the source
      % bucket becomes empty, or the target becomes full
      forall(b1, b2 in buckets where b1 != b2) (
         ((state[step, b1] != state[step+1, b1]) /\ (state[step, b2] != state[step+1, b2])) ->
            (state[step+1,b1] = 0 \/ state[step+1,b1] = capacity[b1] \/
             state[step+1,b2] = 0 \/ state[step+1,b2] = capacity[b2])
     )
   )
;
 
 
output [
  if s = 1 /\ b = 1 then
    "goal_step: " ++ show(goal_step)
  else "" endif ++
  if b = 1 then "\n" else " " endif ++
  show(state[s, b])
  | s in steps, b in buckets
 
]
++ ["\n"];