sbv-7.13: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Documentation.SBV.Examples.Optimization.VM

Description

Solves a VM allocation problem using optimization features

Synopsis

- allocate :: Goal

# Documentation

allocate :: Goal Source #

The allocation problem. Inspired by: http://rise4fun.com/Z3/tutorialcontent/optimization#h25

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