Fast and Exact Synthesis of Application Deployment Plans using Graph Neural Networks and Satisfiability Modulo Theory

Learning-augmented algorithms use machine learning predictions to boost optimization algorithms performance. The extra information incorporated into learning-augmented algorithms is, for example, the input which resembles prior instances, potentially aiding in circumventing the need to compute solutions from scratch or facilitating the utilization of existing solutions for deriving new ones.In previous works, we synthesized leasing cost optimal, subsequently named optimal, Cloud deployment plans by solving the corresponding constrained optimization problem using Satisfiability Modulo Theory (SMT) solvers and symmetry breakers. In this paper, we leverage the previously generated deployment plans to create a model of the deployed application. We employ graph neural networks (GNNs) for this purpose, encoding past deployment plans as graphs, with components and virtual machines as nodes and their interactions as edges. The GNN model trained can learn from historical data to predict optimal assignments by solving the corresponding edge classification problem. These predictions are then used as soft constraints in the exact SMT solver Z3, efficiently guiding the solver towards the optimal solution.We exemplify our approach on a Secure Web Container application.The accompanying material of this paper, as well as the application of our approach to other case studies, is publicly available at https://github.com/SAGE-Project/SAGE-GNN/tree/IJCNN2024.