# Generating Datasets for Real-Time Scheduling on 5G New Radio
## 5 Formulation of the SMT Problem
### Improvement  
Our proposed SMT-based method is shown in Figure 4. The method first checks whether the scheduling problem is unschedulable or not based on Theorem 1. If there may be a solution, then we address the following two subproblems: (1) find the lower bound \(B\) and upper bound \(C\) of \(A\) based on Theorem 2, Algorithm 1, and Equation (11); (2) in the range of \([B,C]\), find the minimum value of \(A\) that makes \(SMT(A)\) satisfiable based on Theorem 3. Invoking this method once can generate one solution. By invoking the method multiple times with different inputs, a large number of solutions can be generated and constitute our dataset. In the following, we present our method in detail. Given a scheduling problem \(V\), \(L\), and \(P\), if the problem satisfied the sufficient condition (Theorem 1), then it must be unschedulable, and the method ends. Otherwise, the method proceeds to the next steps. **Theorem 1** (Sufficient condition for unschedulability). : _For the scheduling problem \(V\), \(L\), and \(P\), if \(\exists m\in[1,M]\), and_  
\[\frac{\sum\limits_{\forall\gamma_{i}\in V^{m}}(4\times m_{i})}{L\times P}>100 \%, \tag{8}\]  
_then the problem must be unschedulable._  
Proof. : Based on the non-conflicting constraint, the utilization of resource \(L\times P\) on each slice perpendicular to the \(Z\) axis cannot be greater than 100%. The \(Z\) axis has a value range of \(m\in[1,M]\). Each \(m\) corresponds to a slice perpendicular to the \(Z\) axis, and \(V^{m}\) contains the packets that use this slice resource. Hence, \(\frac{\sum\limits_{\forall\gamma_{i}\in V^{m}}(4\times m_{i})}{L\times P}\) can be used to calculate the utilization of the slice resource, where 4 represents four resources occupied per transmission. If there exists \(m\) in \([1,M]\), and the corresponding resource utilization is more than 100%, all packets must not be scheduled without confiction. When there is no cover, \(A\) should be 0, i.e., 0 must be the lower bound of \(A\). However, some 5G NR scheduling problems may not be scheduled without covering. In Theorem 2, we will tighten the lower bound \(B\) by analyzing the cases that cannot be scheduled without covering, to reduce the number of times to solve SMT. To prove Theorem 2, we define \(V^{\prime}\) as the set containing packets sorted in decreasing order of number of transmissions, i.e., \(V^{\prime}=\{V^{M},V^{M-1},\ldots,V^{1}\}\), as shown in Figure 5. The packets in each \(V^{m}\) (\(m\in[1,M]\)) can be in any order because \(V^{\prime}\) focuses on the resource usage of packets while the packets in each \(V^{m}\) occupy the same amount of resources. We use \(k\) to represent that, under non-coverable scheduling, the resource requirements for the first \(k\) packets in \(V^{\prime}\) is less than or equal to \(L\times P\), and the resource requirements of the first \(k+1\) packets is greater than \(L\times P\), i.e.,  
\[\sum\limits_{\forall i\in[1,k]}(m^{\prime}_{i}\times 4)\leq L\times P<\sum \limits_{\forall i\in[1,k+1]}(m^{\prime}_{i}\times 4), \tag{9}\]  
Figure 4: Flow chart of our method. where \(V^{m^{\prime}}\) represents the subset containing the \(k\)th packet. In addition, we extend \(w^{0}=0\). Thus, Theorem 2 is as follows. **Theorem 2** (Lower bound of \(A\)). : _For the scheduling problem \(V\), \(L\), and \(P\), the lower bound \(B\) of \(A\) is calculated as follows:_  
\[B=\sum_{\forall m\in[1,m^{\prime})}{(w^{m}\times|V^{m}|)}+w^{m^{\prime}}\times (|V|-k-\sum_{\forall m\in[1,m^{\prime})}{|V^{m}|)}-w^{\frac{L\times P-\sum\limits _{\forall m\in[1,m^{\prime}]}{(w^{m}_{j}\times 4)}}{4}}. \tag{10}\]  
Proof. : Based on the definition of \(k\), in resource \(L\times P\), after the first \(k\) packets are placed, there are no sufficient resources to place the \((k+1)\)th packet. However, perhaps a later packet could be placed. Then, the remaining packets must be covered and considered in the calculation of \(B\).