Skip to main content

A Small Case Study

In collaboration with Anh-Dung Phan.

Problem description​

Use the problem of virtual machine placement as an example. Assume that we have three virtual machines (VMs) which require 100, 50 and 15 GB hard disk respectively. There are three servers with capabilities 100, 75 and 200 GB in that order. Find out a way to place VMs into servers in order to

  • Minimize the number of servers used
  • Minimize the operation cost (the servers have fixed daily costs 10, 5 and 20 USD respectively.)

Boolean encoding​

We start with a Boolean encoding. Let xij denote that VM i is put into server j and yj denote that server j is in use.

The assert-soft command represents MaxSMT which tries to maximize the weighted sum of Boolean expressions belonged to the same id. Since we are doing minimization, negation is needed to take advantage of MaxSMT support.

Integer encoding​

In this example, the Boolean encoding is not really natural. Most of the constraints is of arithmetic form, it makes more sense to express them using integer arithmetic. Here is a similar encoding using integer arithmetic.

The capability constraints and goals are easier to express than those of Boolean encoding. However, we need to add extra constraints to ensure that only 0-1 integers are allowed in the model. It is also interesting to see different results by choosing various ways of combining objectives. You can uncomment the set-option command and take a look at results.