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
language ESSENCE 1.2.0
$ prob116.essence: Vellino's Problem
$ Problem details available in:
$   The OPL Optimization Programming Language
$   Pascal Van Hentenryck
$   MIT Press, January 1999.
$
$ 27 July 2007
$
 
given maxMaterial : int
 
$ Material: there are five different types of materials
$ Colour: there are three different types of bin, distinguished by colour
letting Material be new type enum {glass,plastic,steel,wood,copper},
        Colour be new type enum {red,green,blue}
 
$ quantity: the amount of each material that is required to be placed in bins
$ capacity: each bin type (colour) has a certain capacity
given quantity : function (total) Material --> int(0..),
      capacity : function (total) Colour --> int(0..)
 
$ Bin: bins are represented by an unnamed type. the number of values is the same
$      as the total amount of material that is required
letting Bin be new type of size (sum m : Material . quantity(m))
 
$ colour: each bin is assigned a colour
$ contents: the contents of each bin is a multiset of materials
find colour : function Bin --> Colour,
     contents : function Bin --> mset (maxOccur maxMaterial) of Material
 
$ minimise the number of bins that have colours & materials assigned to them
minimising |defined(colour)|
 
such that
$ every bin that has a colour, must also have a contents, and vice versa
    forAll b : Bin . b in defined(colour) <-> b in defined(contents),
$ the correct amount of each material is spread across all the bins
    forAll m : Material . (sum b in defined(contents) . freq(contents(b),m))
                          = quantity(m),
$ the amount of material in each bin does not exceed its capacity
    forAll b in defined(colour) . |contents(b)| <= capacity(colour(b)),
$ red bins cannot contain plastic or steel
    forAll b in defined(colour) . colour(b) = red ->
                                   !(plastic in contents(b)) /\
                                   !(steel in contents(b)),
$ blue bins cannot contain wood or plastic
    forAll b in defined(colour) . colour(b) = blue ->
                                   !(wood in contents(b)) /\
                                   !(plastic in contents(b)),
$ green bins cannot contain steel or glass
    forAll b in defined(colour) . colour(b) = green ->
                                   !(steel in contents(b)) /\
                                   !(glass in contents(b)),
$ red bins contain at most one wooden component
    forAll b in defined(colour) . colour(b) = red ->
                                   freq(contents(b),wood) <= 1,
$ green bins contain at most two wooden components
    forAll b in defined(colour) . colour(b) = green ->
                                   freq(contents(b),wood) <= 2,
$ wood requires plastic
    forAll b in defined(colour) . wood in contents(b) ->
                                   plastic in contents(b),
$ glass excludes copper
    forAll b in defined(colour) . glass in contents(b) ->
                                   !(copper in contents(b)),
$ copper excludes plastic
    forAll b in defined(colour) . copper in contents(b) ->
                                   !(plastic in contents(b))