Home

Welcome to the OMT-Benchmarks wiki!

Motivation

The development, assessment, and comparison of Optimization Modulo Theory (OMT) algorithms and tools heavily depends on benchmarking. To the best of our knowledge, there is no benchmark environment for OMT, much less one which bears any relation to the number of distinct problem features. We propose a scalable linear, respectively non-linear, constrained optimization problem that is suitable for benchmarking OMT solvers.

This repository provides a Python implementation of the benchmarking environment introduced in the paper: "Constrained Optimization Benchmark for Optimization Modulo Theory: a Cloud Resource Management Problem" by M. Erascu and R. Metes, submitted to SMT2019 workshop.

The reporting of implementation issues as well as suggestions for improvement (or modification) are welcome. Please contact: madalina.erascu___at___e-uvt.ro

Prerequisites

PyChamrm IDE. The project interpreter must be Python 3.6 together with the libraries installing Z3 and ortools.

Installation

Download the project from https://github.com/merascu/Optimization-Modulo-Theory

Getting Started

The environment offers three features:

1. Generation of SMT-LIB files
2. Generation of benchmarks for OMT
3. Statistics

Generation of SMT-LIB files

In the file MainTestFile.py, calling the function

runZ3(app_name, offers_name, encoding_name, option)

where:

• app_name is the file describing the application.
• offers_name is the file containing the VMs offers.
• encoding_name is the encoding name.
• option can be either linear or nonlinear

An example of app_name:

{
"application" : "WordPress",
"components" :[
  {"id": 1, "name" : "WordPress",
    "Compute": {"CPU":2, "Memory": 512},
    "Storage": {"StorageType": "HDD", "StorageSize": 1000},
    "operatingSystem": "Linux"
  },
    {"id": 3, "name" : "DNSLoadBalancer",
    "Compute": {"CPU":4, "Memory": 2048},
    "Storage": {"StorageType": "HDD", "StorageSize": 500},
    "operatingSystem": "Linux"
  }
],
"restrictions" : [{"type":"LowerBound",  "compsIdList":[1], "bound": 3},
                  {"type":"RequireProvideDependency", "alphaCompId":3, "betaCompId":1, "alphaCompIdInstances":7, "betaCompIdInstances":1}
]
}

Short explication:
Compute - numbers of CPU; memory (in MB)
Storage - storage type and storage size (in GB)
operatingSystem - type of operating system
restrictions type :

• LowerBound - a special case when the number instances corresponding to a set of deployed components, should be at least a specified value.
• RequireProvideDependency - a special case of interaction between components is when one component requires some functionalities offered by other components

An example of offers_name:

{ 
  "c64.0m976.0s1.0osLinuxp8.4030000000": {   
    "cpu": 64,  
    "memory": 976000,  
    "storage": 1000,  
    "operatingSystem": "Linux",  
    "price": 8403  
  }
}    

Short explication:
memory in MB
storage in GB
price is in USD

If the option is linear, the encoding_name can be: RealReal, RealBool, IntIntOr, IntIntLessThan, BV, RealPBC or RealPBCMultiObjectives.
If the option is linear, the encoding_name can be: RealReal, RealBool, IntIntOr, IntIntLessThan or BV.

Short explication:
RealReal - all variables have type Real
IntIntOr/IntIntLessThan - all variables have type Int
BV - all variables are bitvectors

More information:

will output (in a suitable directory):

• a CSV file with running statistics (only for Z3)
• an SMT-LIB compliant file with the optimization problem (Z3 or OptiMathSAT compliant)
• an output file with a model (if this is the case) for the optimization problem. If solving the problem takes more than 40 minutes, then no such file will be output.

Generation of benchmarks for OMT

In the file MainTestFile.py, there are two functions that can be called to generate benchmark

processingBenchmarks_Z3(input_path, output_path, option) [1]
processingBenchmarks_OptiMathSAT(input_path, output_path, option) [2]

where:

• input_path is the path from where the SMT files will be processed to be converted into benchmarks
• output_path is the directory where benchmarks will be saved
• option can be either linear or nonlinear

will output:

• an SMT-LIB compliant file with the optimization problem with a particular format, namely SMT-LIB format for benchmarks

It is obvious that the function [1] is used to generate the benchmarks for Z3, respectively the function [2] for OptiMathSAT.

Statistics

In the file MainTestFile.py, calling the function

statisticsBest(path_read, path_sol, option)

where:

• path_read is the path from where the csv files will be used to obtain output files
• path_sol is the directory where output files will be saved
• option can be either linear or nonlinear

will output:

• a CSV file, where, next to each application with the number of offers, all the encodings used to resolve the optimization problem are in ascending order according to the average execution time. After each encoding, both the average execution times and their standard deviation appear.
• a CSV file with a count on each encoding used to resolve the optimization problem for all our SMT files