fitting VMs into hosts

vmonhost.scm

;; declare a cartesian product of host server and VM
;; three VMs x1, x2, x3 and three hosts y1, y2, y3
(declare-const x11 Int) ; VM x1 might be on host y1
(declare-const x12 Int) ; VM x1 might be on host y2
(declare-const x13 Int)
(declare-const x21 Int) ; VM x2 might be on host y1
(declare-const x22 Int)
(declare-const x23 Int)
(declare-const x31 Int)
(declare-const x32 Int)
(declare-const x33 Int) ; VM x3 might be on host y3

;; declare the hosts as Int
(declare-const y1 Int)
(declare-const y2 Int)
(declare-const y3 Int)

;; the solution grid cannot be negative
;; each combination of VM and host must be zero or more
(assert (and (>= x11 0) (>= x12 0) (>= x13 0)
	     (>= x21 0) (>= x22 0) (>= x23 0)
	     (>= x31 0) (>= x32 0) (>= x33 0)))

;; There's no more than one of each host server.
(assert (and (<= y1 1) (<= y2 1) (<= y3 1)))

;; the sum of the count of each VM on all hosts is one
;; that is, VM x1 must exist on one of the hosts, but no more or less than one
(assert (= (+ x11 x12 x13) 1)) ; VM x1 must exist somewhere
(assert (= (+ x21 x22 x23) 1)) ; VM x2 must exist somewhere
(assert (= (+ x31 x32 x33) 1)) ; VM x3 must exist somewhere

;; ???
(assert (and (>= y1 x11) (>= y1 x21) (>= y1 x31)))
(assert (and (>= y2 x12) (>= y2 x22) (>= y2 x32)))
(assert (and (>= y3 x13) (>= y3 x23) (>= y3 x33)))

;; server y1 has 100 GB space, y2 has 75GB, y3 has 200GB
;; VM x1 requires 100, x2 requires 50, x3 requires 15
(assert (<= (+ (* 100 x11) (* 50 x21) (* 15 x31)) (* 100 y1)))
(assert (<= (+ (* 100 x12) (* 50 x22) (* 15 x32)) (* 75 y2)))
(assert (<= (+ (* 100 x13) (* 50 x23) (* 15 x33)) (* 200 y3)))

;; ??? does this mean use the fewest servers? or is this another cost minimizer?
(minimize (+ y1 y2 y3))
;; server y1 costs $10 a day, y2 costs $5/day, y3 costs $20 a day
;; minimize the daily host costs
(minimize (+ (* 10 y1) (* 5 y2) (* 20 y3)))

;;(set-option :opt.priority pareto)
;; is there a solution?
(check-sat)
;; display the best solution
(get-model)
(get-objectives)