Abstract:
Optimization Modulo Theories (OMT) is a computational approach that extends Satisfiability Modulo Theories (SMT) to address optimization problems. While SMT focuses on determining the satisfiability of logical formulas within specific theories (such as linear arithmetic, arrays, or bit-vectors), OMT aims to find an optimal solution for these formulas under a given objective function. Popular OMT solvers include Z3 [1] and OptiMathSAT [2]. We will use Z3 in this tutorial.
The tutorial is divided into two parts. In the first part, we will introduce toy examples demonstrating OMT, which can be manually written using SMT-LIB syntax [3]. For more complex problems, the APIs provided by OMT tools are essential. The second part will illustrate this with a case study on the automated deployment of component-based applications in the Cloud. This problem involves allocating virtual machine (VM) offers from various Cloud Providers, ensuring that constraints from component interactions and hardware/software requirements are met, while optimizing performance objectives (e.g., minimizing costs). This can be formulated as a constraint optimization problem, enabling automatic optimization in principle. However, when dealing with a large set of VM offers (several hundreds), the computational demand becomes significant, making automatic optimization impractical with current general OMT tools.
We addressed this challenge by methodically analyzing the problem to identify search space reduction methods. These methods leverage:
1) Symmetries in the general Cloud deployment problem, the graph representation associated with structural constraints specific to each application, and their combinations (based on paper [4]).
2) Historical data and the graph-based representation of a particular application to extract soft constraints from edge classification predictions based on paper [5]).
References:
[1] https://github.com/Z3Prover/z3
[2] https://optimathsat.disi.unitn.it/
[4] M Erascu, F Micota, D Zaharie, “Scalable optimal deployment in the cloud of component-based applications using optimization modulo theory, mathematical programming and symmetry breaking”, Journal of Logical and Algebraic Methods in Programming 121, 100664
[5] E Laitin and M Erascu, “Fast and Exact Synthesis of Application Deployment Plans Using Graph Neural Networks and Satisfiability Modulo Theory”, accepted at 2024 International Joint Conference on Neural Networks (IJCNN).
Short Bio:
Mădălina ERAŞCU is Associate Professor in the Department of Computer Science of West University of Timisoara, Romania and Researcher at Institute e-Austria, Timisoara, Romania. She holds a PhD in Technical Sciences from Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria. Her PhD thesis was advised by Professor Tudor Jebelean and Professor Hoon Hong and deals with the (semi-)automatic analysis and synthesis of programs using computational logic and polynomial algebra algorithms. She also holds a M.Sc. from Johannes Kepler University (2008) and a B.Sc. from West University of Timisoara (2006), both in computer science. Her master’s and bachelor’s theses were partly realized in the framework of the software companies Mindbreeze Software GmbH and, respectively, SC memIQ SRL.
In 2021, she was awarded The Fulbright-RAF Scholar Award in the field of Entrepreneurship & Entrepreneurial Studies for spending the Spring Semester of 2022 at University of Rochester, AIN Center for Entrepreneurship with the goals of study and independent research, curriculum development, classroom observation and participation in community-based entrepreneurial activities.
In 2010, she was awarded the competitive DOC-fFORTE-fellowship of the Austrian Academy of Sciences (June 2011 – November 2012). In the framework of Marshall Plan Foundationscholarship, she spent five months (January – June 2011) at North Carolina State University, Raleigh, USA, working under the supervision of Professor Hoon Hong.
She is interested in developing algorithmic methods for building and maintaining reliable algorithms. To achieve this goal, she combines theoretical research in formal methods, satisfiability checking and symbolic computation motivated by practical applications in Cloud Computing, Big Data and Machine/Deep Learning.
She was involved in several projects funded by European Commission and other research funding agencies (in Romania and Austria), as local team leader, member or PI.
As an Innovation Researcher at Continental Automotive Romania SRL she was involved in the concept and development of a Sensor Error Model prototype as well as in Patent writing.
