Joint routing and scheduling with SMT

Abstract

Real-time communication over Ethernet networks are of growing importance for industrial applications. With the newly developed IEEE 802.1Qbv standard, new tools for guaranteeing timely boundaries for communication are available. While this standard specifies the mechanisms in place for guaranteeing the timeliness of transmissions, it falls short of defining algorithms to compute routes and schedules. Traditionally the routing problem and scheduling problem have been tackled independently. However these problems are strongly connected and solving them independently excludes feasible solutions. We provide an SMT formulation of the joint routing and scheduling problem. We implement this formulation to solve various different scheduling problems. We showcase and compare our SMT-Based solution to a similar ILP-Based solution.