## [SMT][Z3] Packing virtual machines into servers

You've got these servers (all in GBs):

     RAM storage
srv0  2     100
srv1  4     800
srv2  4    1000
srv3 16    8000
srv4  8    3000
srv5 16    6000
srv6 16    4000
srv7 32    2000
srv8  8    1000
srv9 16   10000
srv10  8    1000


And you're going to put these virtual machines to servers:

    RAM storage
VM0  1     100
VM1 16     900
VM2  4     710
VM3  2     800
VM4  4    7000
VM5  8    4000
VM6  2     800
VM7  4    2500
VM8 16     450
VM9 16    3700
VM10 12    1300


The problem: use as small number of servers, as possible. Fit VMs into them in the most efficient way, so that the free RAM/storage would be minimal.

This is like knapsack problem. But the classic knapsack problem is about only one dimension (weight or size). We've two dimensions here: RAM and storage. This is called "multidimensional knapsack problem".

Another problem we will solve here is a bin packing problem.

from z3 import *
import itertools

# RAM, storage, both in GB
servers=[(2, 100),
(4, 800),
(4, 1000),
(16, 8000),
(8, 3000),
(16, 6000),
(16, 4000),
(32, 2000),
(8, 1000),
(16, 10000),
(8, 1000)]

# RAM, storage
vms=[(1, 100),
(16, 900),
(4, 710),
(2, 800),
(4, 7000),
(8, 4000),
(2, 800),
(4, 2500),
(16, 450),
(16, 3700),
(12, 1300)]

vms_total=len(vms)

VM_RAM_t=sum(map(lambda x: x[0], vms))
VM_storage_t=sum(map(lambda x: x[1], vms))

print "RAM total we need", VM_RAM_t
print "storage total we need", VM_storage_t

def try_to_fit_into_servers(servers_to_be_used):
t=len(servers_to_be_used)
# for each server:
RAM_allocated=[Int('srv%d_RAM_allocated' % i) for i in range(t)]
storage_allocated=[Int('srv%d_storage_allocated' % i) for i in range(t)]
# which server this VM occupies?
VM_in_srv=[Int('VM%d_in_srv' % i) for i in range(vms_total)]

# how much RAM/storage we have in picked servers, total?
RAM_t=0
storage_t=0
for i in range(t):
RAM_t=RAM_t+servers[servers_to_be_used[i]][0]
storage_t=storage_t+servers[servers_to_be_used[i]][1]
# skip if the sum of RAM/storage in picked servers is too small:
if VM_RAM_t>RAM_t or VM_storage_t>storage_t:
return

print "trying to fit VMs into servers:", servers_to_be_used,

s=Solver()

# all VMs must occupy some server:
for i in range(vms_total):
if s.check()==sat:
print "sat"
print "* solution (%d servers):" % t
m=s.model()

for i in range(t):
print "srv%d (total=%d/%d):" % (servers_to_be_used[i], servers[servers_to_be_used[i]][0], servers[servers_to_be_used[i]][1]),
for v in range(vms_total):
if m[VM_in_srv[v]].as_long()==i:
print "VM%d (%d/%d)" % (v, vms[v][0], vms[v][1]),
print "allocated on srv=%d/%d" % (m[RAM_allocated[i]].as_long(), m[storage_allocated[i]].as_long()),
print "free on srv=%d/%d" % (servers[servers_to_be_used[i]][0] - m[RAM_allocated[i]].as_long(), servers[servers_to_be_used[i]][1] - m[storage_allocated[i]].as_long()),
print ""
print "total in all servers=%d/%d" % (RAM_t, storage_t)
print "allocated on all servers=%d%%/%d%%" % ((float(VM_RAM_t)/float(RAM_t))*100, (float(VM_storage_t)/float(storage_t))*100)
print ""
return True
else:
print "unsat"
return False

found_solution=False
for servers_to_pick in range(2, len(servers)+1):

# we use Python itertools to find all combinations
# in other words, pick $servers_to_pick$ servers from all servers, and enumerate all possible ways to choose from them.
for servers_to_be_used in itertools.combinations(range(len(servers)), r=servers_to_pick):
if try_to_fit_into_servers(servers_to_be_used):
found_solution=True
# after we've got some solutions for $servers_to_pick$, stop:
if found_solution:
break



( https://github.com/DennisYurichev/yurichev.com/blob/master/blog/VM_packing/VM_pack.py (syntax highlighed version) )

The result:

RAM total we need 85
storage total we need 22260
trying to fit VMs into servers: (3, 4, 5, 6, 7) unsat
trying to fit VMs into servers: (3, 4, 5, 7, 9) sat
* solution (5 servers):
srv3 (total=16/8000): VM2 (4/710) VM3 (2/800) VM5 (8/4000) VM6 (2/800) allocated on srv=16/6310 free on srv=0/1690
srv4 (total=8/3000): VM0 (1/100) VM7 (4/2500) allocated on srv=5/2600 free on srv=3/400
srv5 (total=16/6000): VM9 (16/3700) allocated on srv=16/3700 free on srv=0/2300
srv7 (total=32/2000): VM1 (16/900) VM8 (16/450) allocated on srv=32/1350 free on srv=0/650
srv9 (total=16/10000): VM4 (4/7000) VM10 (12/1300) allocated on srv=16/8300 free on srv=0/1700
total in all servers=88/29000
allocated on all servers=96%/76%

trying to fit VMs into servers: (3, 4, 6, 7, 9) sat
* solution (5 servers):
srv3 (total=16/8000): VM2 (4/710) VM3 (2/800) VM5 (8/4000) VM6 (2/800) allocated on srv=16/6310 free on srv=0/1690
srv4 (total=8/3000): VM0 (1/100) VM7 (4/2500) allocated on srv=5/2600 free on srv=3/400
srv6 (total=16/4000): VM9 (16/3700) allocated on srv=16/3700 free on srv=0/300
srv7 (total=32/2000): VM1 (16/900) VM8 (16/450) allocated on srv=32/1350 free on srv=0/650
srv9 (total=16/10000): VM4 (4/7000) VM10 (12/1300) allocated on srv=16/8300 free on srv=0/1700
total in all servers=88/27000
allocated on all servers=96%/82%

trying to fit VMs into servers: (3, 5, 6, 7, 9) sat
* solution (5 servers):
srv3 (total=16/8000): VM0 (1/100) VM5 (8/4000) VM6 (2/800) VM7 (4/2500) allocated on srv=15/7400 free on srv=1/600
srv5 (total=16/6000): VM10 (12/1300) allocated on srv=12/1300 free on srv=4/4700
srv6 (total=16/4000): VM9 (16/3700) allocated on srv=16/3700 free on srv=0/300
srv7 (total=32/2000): VM1 (16/900) VM8 (16/450) allocated on srv=32/1350 free on srv=0/650
srv9 (total=16/10000): VM2 (4/710) VM3 (2/800) VM4 (4/7000) allocated on srv=10/8510 free on srv=6/1490
total in all servers=96/30000
allocated on all servers=88%/74%

trying to fit VMs into servers: (3, 5, 7, 8, 9) unsat
trying to fit VMs into servers: (3, 5, 7, 9, 10) unsat
trying to fit VMs into servers: (3, 6, 7, 8, 9) unsat
trying to fit VMs into servers: (3, 6, 7, 9, 10) unsat
trying to fit VMs into servers: (4, 5, 6, 7, 9) unsat
trying to fit VMs into servers: (5, 6, 7, 8, 9) unsat
trying to fit VMs into servers: (5, 6, 7, 9, 10) unsat



Choose any solution you like...

Further work: storage can be both HDD and/or SDD. That would add 3rd dimension. Or maybe number of CPU cores, network bandwidth, etc...