-----------------------------------------------------------------------------
-- |
-- 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
-----------------------------------------------------------------------------

{-# LANGUAGE CPP #-}

{-# OPTIONS_GHC -Wall -Werror #-}

module Documentation.SBV.Examples.Optimization.VM where

import Data.SBV

#ifndef HADDOCK
-- $setup
-- >>> -- For doctest purposes only:
-- >>> import Data.SBV
#endif

-- | 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 :: ConstraintSet
allocate = do
    -- xij means VM i is running on server j
    x1@[x11, x12, x13] <- [String] -> Symbolic [SBool]
sBools [String
"x11", String
"x12", String
"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 [SBool]
rs = [SInteger] -> SInteger
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([SInteger] -> SInteger) -> [SInteger] -> SInteger
forall a b. (a -> b) -> a -> b
$ (SBool -> SInteger -> SInteger)
-> [SBool] -> [SInteger] -> [SInteger]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\SBool
r SInteger
c -> SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
r SInteger
c SInteger
0) [SBool]
rs [SInteger
100, SInteger
50, SInteger
15]

    -- The capacity on each server is respected
    let capacity1 = [SBool] -> SInteger
need [SBool
x11, SBool
x21, SBool
x31]
        capacity2 = [SBool] -> SInteger
need [SBool
x12, SBool
x22, SBool
x32]
        capacity3 = [SBool] -> SInteger
need [SBool
x13, SBool
x23, SBool
x33]

    constrain $ capacity1 .<= 100
    constrain $ capacity2 .<=  75
    constrain $ capacity3 .<= 200

    -- compute #of servers running:
    let y1 = [SBool] -> SBool
sOr [SBool
x11, SBool
x21, SBool
x31]
        y2 = [SBool] -> SBool
sOr [SBool
x12, SBool
x22, SBool
x32]
        y3 = [SBool] -> SBool
sOr [SBool
x13, SBool
x23, SBool
x33]

        b2n SBool
b = SBool -> a -> a -> a
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
b a
1 a
0

    let noOfServers = [SInteger] -> SInteger
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([SInteger] -> SInteger) -> [SInteger] -> SInteger
forall a b. (a -> b) -> a -> b
$ (SBool -> SInteger) -> [SBool] -> [SInteger]
forall a b. (a -> b) -> [a] -> [b]
map SBool -> SInteger
forall {a}. (Mergeable a, Num a) => SBool -> a
b2n [SBool
y1, SBool
y2, SBool
y3]

    -- minimize # of servers
    minimize "noOfServers" (noOfServers :: SInteger)

    -- cost on each server
    let cost1 = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
y1 SInteger
10 SInteger
0
        cost2 = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
y2  SInteger
5 SInteger
0
        cost3 = SBool -> SInteger -> SInteger -> SInteger
forall a. Mergeable a => SBool -> a -> a -> a
ite SBool
y3 SInteger
20 SInteger
0

    -- minimize the total cost
    minimize "cost" (cost1 + cost2 + cost3 :: SInteger)