Boolean encoding of Virtual Machine placement problem

ComplexConstraints.fs

let mkBoolLe coeffs args k = context.MkPBLe(coeffs, args, k)
let assertHard (b: BoolExpr) = solver.Assert(b)

// Each server has fulfilled capability constraints
for j in 1..n do
    let yj = ys.[j-1]
    let capabilityJ = capabilities.[j-1]
    let coeffs = 
        [| 
            yield! requirements
            yield -capabilityJ
        |]
    let bs = 
        [| 
            yield! xs |> Array.map (fun xi -> xi.[j-1])
            yield yj
        |]
    assertHard (mkBoolLe coeffs bs 0)

Goals.fs

let serverNumGoal =
    seq {
        for j in 1..n ->
            let yj = ys.[j-1]
            assertSoft (-. yj) 1u "num_servers"
    }
    |> Seq.last

let costGoal =
    seq {
        for j in 1..n ->
            let yj = ys.[j-1]
            let cost = uint32 costs.[j-1]
            assertSoft (-. yj) cost "costs"
    }
    |> Seq.last

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

Results.txt

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

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

SimpleConstraints.fs

let (=>.) x y = context.MkImplies(x, y)
let (&&.) x y = context.MkAnd(x, y)
let ( *. )  (x: IntNum) (y: ArithExpr) = context.MkMul(x, y)
let (~-.) (b: BoolExpr) = context.MkNot(b)
let (=.) (x: ArithExpr) (y: ArithExpr) = context.MkEq(x, y)
let (<=.)  (x: ArithExpr) (y: ArithExpr) = context.MkLe(x, y)

let mkAtmost k bs =
    context.MkAtMost(bs, uint32 k)
let mkAtLeast k bs =
    let n = Array.length bs
    context.MkAtMost(Array.map (~-.) bs, uint32 (n - k))

let assertHard (b: BoolExpr) = solver.Assert(b)

// Place each VM on exactly one server
for xi in xs do        
    assertHard (mkAtmost 1 xi &&. mkAtLeast 1 xi)

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

VariableDeclaration.fs

let xs =
    [| 
        for i in 1..m ->
          [| for j in 1..n -> boolOf (sprintf "x_%i_%i" i j) |] 
    |]

let ys =
    [| for j in 1..n -> boolOf (sprintf "y_%i" j) |]