Virtual Network Embedding as Boolean Satisfiability

We address the Virtual Network Embedding (VNE) problem in which the task is to map a virtual network onto a given physical substrate network so that the CPU and bandwidth capacity constraints are met. Following the success of Boolean Satisfiability (SAT) methods in areas such as Multi-Agent Path Finding (MAPF), we propose in this paper a novel SAT-based approach for solving the VNE problem. As in MAPF, the various constraints that define the VNE problem are encoded into the SAT models incrementally and via lazy refinements so as to keep the models simple. We also propose various model relaxations and concomitant solution extraction post-processing procedures. Through experiments, we show that our SAT-based approach outperforms other state-of-the-art approaches on a number of VNE instances.