[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):
        s.add(And(VM_in_srv[i]>=0, VM_in_srv[i]=0, RAM_allocated[i]<=servers[servers_to_be_used[i]][0]))
        s.add(And(storage_allocated[i]>=0, storage_allocated[i]<=servers[servers_to_be_used[i]][1]))
    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

# how many servers we need? start with 2:
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.
    # see also: https://en.wikipedia.org/wiki/Combination
    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...


→ [list of blog posts]

Please drop me email about any bug(s) and suggestion(s): dennis(@)yurichev.com.