Integer encoding of Virtual Machine placement problem

Constraints.fs

// Place each VM on exactly one server
for xi in xs do        
    assertHard (add xi =. mkInt 1)

// A used server always has at least a VM on it
for j in 1..n do
    let yj = ys.[j-1]
    xs |> Array.iter (fun xi -> 
            let xij = xi.[j-1]
            assertHard (yj >=. xij))

// Each server has fulfilled capability constraints
for j in 1..n do
    let yj = ys.[j-1]
    let capability = capabilities.[j-1]
    let sum =
        xs |> Array.map (fun xi -> xi.[j-1])               
           |> Array.map2 (fun requirement xij -> requirement *. xij) requirements
           |> add
    assertHard (sum <=. capability *. yj)

Goals.fs

let serverNumGoal =
    minOf (add ys)

let costGoal =
    minOf (ys |> Array.map2 ( *. ) costs |> add)

match solver.Check() with
| Status.SATISFIABLE ->
    printfn "Number of servers: min --> %O" (solver.GetUpper(serverNumGoal))
    printfn "Costs: min --> %O" (solver.GetUpper(costGoal))
| _ ->
    printfn "Can't find a solution. Please recheck your constraints."

Initialization.fs

use context = new Context()
let solver = context.MkOptimize()
let m = requirements.Length
let n = capabilities.Length

let intOf (s: string) = context.MkIntConst s
let mkInt (i: int) = context.MkInt i
let add (ts: ArithExpr []) = context.MkAdd(ts)

let (&&.) x y = context.MkAnd(x, y)
let ( *. )  (x: int) (y: ArithExpr) = context.MkMul(context.MkInt x, y)
let (=.) (x: ArithExpr) (y: ArithExpr) = context.MkEq(x, y)
let (<=.)  (x: ArithExpr) (y: ArithExpr) = context.MkLe(x, y)
let (>=.)  (x: ArithExpr) (y: ArithExpr) = context.MkGe(x, y)

let assertHard (b: BoolExpr) = solver.Assert(b)
let minOf x = solver.MkMinimize(x)

Params.fs

let param = context.MkParams()
param.Add("priority", context.MkSymbol("pareto"))
solver.Parameters <- param

Results.txt

val problem : PlacementData = {DiskRequirement = [|100; 50; 15|];
                               ServerCapabilities = [|100; 75; 200|];
                               ServerDailyCosts = [|10; 5; 20|];}

* Lexicographic combination:

Number of servers: min --> 1
Costs: min --> 20

* Box combination:

Number of servers: min --> 1
Costs: min --> 15

* Pareto combination:

Number of servers: min --> 2
Costs: min --> 15

VariableDeclaration.fs

let xs =
    [| 
        for i in 1..m ->
          [| for j in 1..n ->
                let xij = intOf (sprintf "x_%i_%i" i j)
                assertHard ((xij >=. mkInt 0) &&. (xij <=. mkInt 1))
                xij :> ArithExpr |] 
    |]

let ys =
    [| for j in 1..n -> 
            let yj = intOf (sprintf "y_%i" j)
            assertHard (yj <=. mkInt 1)
            yj :> ArithExpr |]