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
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
/*
 
  Water buckets problem in Comet.
 
  From 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
  """
 
  Translation from the OPL code at
  http://www.dis.uniroma1.it/~tmancini/index.php?problemid=018&solver=OPL&spec=BASE&currItem=research.publications.webappendices.csplib2x.problemDetails#listing
 
 
  Compare with the MIP model http://www.hakank.org/3_jugs.co
  and the MiniZinc version of this model
   
 
  This Comet model was created by Hakan Kjellerstrand (hakank@gmail.com)
  Also, see my Comet page: http://www.hakank.org/comet/
 
 */
 
// Licenced under CC-BY-4.0 : http://creativecommons.org/licenses/by/4.0/
 
import cotfd;
 
int t0 = System.getCPUTime();
 
int nb_buckets = 3;
int max_step = 10;
range buckets = 1..nb_buckets;
range steps = 1..max_step; 
 
int capacity[buckets] = [8,5,3];
int start[buckets]= [8,0,0];
int goal[buckets]= [4,4,0];
 
 
Solver<CP> m();
 
// Assertions
forall(b in buckets) {
  assert(start[b] <= capacity[b] &&
         goal[b] <= capacity[b]);
}
assert( (sum(b in buckets)(start[b]) == sum(b in buckets)(goal[b])));
 
 
 
// 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
var<CP>{int} state[s in steps,b in buckets](m, 0..capacity[b]);
var<CP>{int} goal_step(m, 1..max_step); // Objective function
 
 // For the AUX constraint, see below.
var<CP>{bool} change[1..max_step-1, buckets](m);
 
Integer num_solutions(0);
 
minimize<m> goal_step subject to {
 
  forall(b in buckets) {
    // C1: At beginning, buckets contain the amount of water specified by
    //     function start
    m.post(state[1,b]==start[b]);
 
 
    // C2: At the end, buckets contain the amount of water specified
    //     by function goal
 
    m.post(state[goal_step,b] == goal[b]);
 
    // hakank: This works as well
    /*
    forall(i in 1..max_step)
      m.post(i == goal_step => state[i, 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)
    m.post(sum(b in buckets)(state[step,b] != state[step+1, b]) == 2);
     
    // C4: The overall amount of water is the same at each time step
    m.post(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 in buckets, b2 in buckets : b1 != b2) {
      m.post(
             (
              (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]
              )
             );
    }
 
  }
 
  // From the second version
  // http://www.dis.uniroma1.it/~tmancini/index.php?problemid=018&solver=OPL&spec=AUX&currItem=research.publications.webappendices.csplib2x.problemDetails#listing
  // AUX: Addition of auxiliary predicates
  // Auxiliary predicate stores, for each time step, which buckets change
  // their amount of water wrt the next one
  forall(step in 1..max_step-1, b in buckets) {
     m.post(change[step,b] == (state[step,b] != state[step+1,b]));
   }
 
   
 
} using {
       
  label(m);
 
  num_solutions := num_solutions + 1;
 
  cout << "goal_step: " << goal_step << endl;
  forall(s in steps) {
    if (s <= goal_step) {
      forall(b in buckets) {
        cout << state[s,b] << " ";
      }
      cout << endl;
    }
  }
  cout << endl;
     
 
}
 
cout << "\nnum_solutions: " << num_solutions << endl;
     
int t1 = System.getCPUTime();
cout << "time:      " << (t1-t0) << endl;
cout << "#choices = " << m.getNChoice() << endl;
cout << "#fail    = " << m.getNFail() << endl;
cout << "#propag  = " << m.getNPropag() << endl;