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
|
-----------------------------------------------------------------------------
-- |
-- Module : Documentation.SBV.Examples.Optimization.VM
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Solves a VM allocation problem using optimization features
-----------------------------------------------------------------------------
{-# OPTIONS_GHC -Wall -Werror #-}
module Documentation.SBV.Examples.Optimization.VM where
import Data.SBV
-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Data.SBV
-- | Computer allocation problem:
--
-- - We have three virtual machines (VMs) which require 100, 50 and 15 GB hard disk respectively.
--
-- - There are three servers with capabilities 100, 75 and 200 GB in that order.
--
-- - Find out a way to place VMs into servers in order to
--
-- - Minimize the number of servers used
--
-- - Minimize the operation cost (the servers have fixed daily costs 10, 5 and 20 USD respectively.)
--
-- We have:
--
-- >>> optimize Lexicographic allocate
-- Optimal model:
-- x11 = False :: Bool
-- x12 = False :: Bool
-- x13 = True :: Bool
-- x21 = False :: Bool
-- x22 = False :: Bool
-- x23 = True :: Bool
-- x31 = False :: Bool
-- x32 = False :: Bool
-- x33 = True :: Bool
-- noOfServers = 1 :: Integer
-- cost = 20 :: Integer
--
-- That is, we should put all the jobs on the third server, for a total cost of 20.
allocate :: ConstraintSet
allocate = do
-- xij means VM i is running on server j
x1@[x11, x12, x13] <- sBools ["x11", "x12", "x13"]
x2@[x21, x22, x23] <- sBools ["x21", "x22", "x23"]
x3@[x31, x32, x33] <- sBools ["x31", "x32", "x33"]
-- Each job runs on exactly one server
constrain $ pbStronglyMutexed x1
constrain $ pbStronglyMutexed x2
constrain $ pbStronglyMutexed x3
let need :: [SBool] -> SInteger
need rs = sum $ zipWith (\r c -> ite r c 0) rs [100, 50, 15]
-- The capacity on each server is respected
let capacity1 = need [x11, x21, x31]
capacity2 = need [x12, x22, x32]
capacity3 = need [x13, x23, x33]
constrain $ capacity1 .<= 100
constrain $ capacity2 .<= 75
constrain $ capacity3 .<= 200
-- compute #of servers running:
let y1 = sOr [x11, x21, x31]
y2 = sOr [x12, x22, x32]
y3 = sOr [x13, x23, x33]
b2n b = ite b 1 0
let noOfServers = sum $ map b2n [y1, y2, y3]
-- minimize # of servers
minimize "noOfServers" (noOfServers :: SInteger)
-- cost on each server
let cost1 = ite y1 10 0
cost2 = ite y2 5 0
cost3 = ite y3 20 0
-- minimize the total cost
minimize "cost" (cost1 + cost2 + cost3 :: SInteger)
|
