Generating Datasets for Real-Time Scheduling on 5G New Radio

A 5G system is an advanced solution for industrial wireless motion control. However, because the scheduling model of 5G new radio (NR) is more complicated than those of other wireless networks, existing real-time scheduling algorithms cannot be used to improve the 5G performance. This results in NR resources not being fully available for industrial systems. Supervised learning has been widely used to solve complicated problems, and its advantages have been demonstrated in multiprocessor scheduling. One of the main reasons why supervised learning has not been used for 5G NR scheduling is the lack of training datasets. Therefore, in this paper, we propose two methods based on optimization modulo theories (OMT) and satisfiability modulo theories (SMT) to generate training datasets for 5G NR scheduling. Our OMT-based method contains fewer variables than existing work so that the Z3 solver can find optimal solutions quickly. To further reduce the solution time, we transform the OMT-based method into an SMT-based method and tighten the search space of SMT based on three theorems and an algorithm. Finally, we evaluate the solution time of our proposed methods and use the generated dataset to train a supervised learning model to solve the 5G NR scheduling problem. The evaluation results indicate that our SMT-based method reduces the solution time by [Formula: see text] compared to existing ones, and the supervised learning algorithm achieves better scheduling performance than other polynomial-time algorithms.