Loading [Contrib]/a11y/accessibility-menu.js
  1. CSPLib
  2. Problems
  3. prob018
  4. Models
  5. water_buckets.essence

018: Water Bucket Problem

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
language Essence 1.3
 
$ You are given an 8 pint bucket of water, and
$ two empty buckets which can contain 5 and 3 pints respectively.
$ You are required 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).
 
letting buckets be domain int(3,5,8)
 
letting initialState be function(3 --> 0, 5 --> 0, 8 --> 8)
letting finalState   be function(3 --> 0, 5 --> 4, 8 --> 4)
 
letting HORIZON be 10
 
 
find actions : sequence (maxSize HORIZON) of (buckets, buckets, int(1..8))
find states  : sequence (maxSize HORIZON) of function (total) buckets --> int(0..max(`buckets`))
 
$ action i transforms state i to state i+1
such that |actions| = |states| - 1
 
$ cannot pour from the a bucket to itself
such that forAll (i, (bFrom, bTo, amount)) in actions . bFrom != bTo
 
$ can only pour if there is enough water
such that forAll (i, (bFrom, bTo, amount)) in actions . amount <= states(i)(bFrom)
 
$ bucket capacity
such that forAll (i, f) in states . forAll b : buckets . f(b) <= b
 
$ preservation of water
such that forAll (i, (bFrom, bTo, amount)) in actions . states(i)(bFrom) - amount = states(i+1)(bFrom)
such that forAll (i, (bFrom, bTo, amount)) in actions . states(i)(bTo) + amount = states(i+1)(bTo)
such that forAll (i, (bFrom, bTo, amount)) in actions .
            forAll b : buckets . !(b in {bFrom, bTo}) -> states(i)(b) = states(i+1)(b)
 
$ after an action, either the source bucket is empty
$                      or the target bucket is full
such that forAll (i, (bFrom, bTo, amount)) in actions . states(i+1)(bFrom) = 0 \/
                                                        states(i+1)(bTo) = bTo
 
$ initial and final state
such that states(1) = initialState
such that states(|states|) = finalState
 
$ minimise the number of actions
find nbActions : int(0..HORIZON)
such that nbActions = |actions|
minimising nbActions