# Generating Datasets for Real-Time Scheduling on 5G New Radio
## 5 Formulation of the SMT Problem
### Improvement
Algorithm 1 first initializes the variables (line 1): \(obj\) is the objective value (Equation (4)), i.e., the upper bound \(C\); \((x,y)\) are the coordinates that our left-top strategy is checking, and the initial value is \((0,L-1)\). The array \(S[x][y][z]\) marks whether resources are occupied by packets. If \(S[x][y][z]=1\), the corresponding resource is occupied. To reduce resource fragmentations, we sort all packets of \(V\) in descending order of the number of transmissions. If multiple packets have the same number of transmissions, the packet with long transmission time is queued first. Then, the sorted packets are contained in the set \(V^{\prime\prime}\) (line 2) and also placed in the same order (line 3). Function \(LT(v_{i}^{\prime\prime},S,x,y,0)\) represents that, given the resource occupation \(S[\,]\,[\,]\,[\,]\), the left-top strategy searches for available places for \(v_{i}^{\prime\prime}\) starting from the coordinates \((x,y)\), and the last parameter means that no packets are allowed to be covered. If the last parameter is 1, then packets can be covered. The coordinates \((x_{i}^{\prime\prime},y_{i}^{\prime\prime})\) returned by \(LT(v_{i}^{\prime\prime},S,x,y,0)\) is the place of \(v_{i}^{\prime\prime}\). Then, the corresponding \(S[\,]\,[\,]\,[\,]\) is updated (line 5), \(v_{i}^{\prime\prime}\) is removed from \(V^{\prime\prime}\) (line 6), and \((x,y)\) is modified to search for the next place (line 7). If \(LT(v_{i}^{\prime\prime},S,x,y,0)\) does not return available coordinates, \(v_{i}^{\prime\prime}\) cannot be placed without covering and remains in \(V^{\prime\prime}\). After all packets of \(V^{\prime\prime}\) are processed, if \(V^{\prime\prime}\) is empty (line 8), then the algorithm finishes, and the objective value is zero because no packets are covered (line 9); otherwise, the remaining packets in \(V^{\prime\prime}\) are placed again (line 11). The remaining packets can be covered, and \(LT(v_{i}^{\prime\prime},S,x,y,1)\) is invoked to search for an available place (line 13). If there is an available place, then the packet is placed, and \(S[\,]\,[\,]\,[\,]\), \(x\), \(y\), and \(obj\) are updated (lines 14-16); otherwise, the algorithm cannot find an available schedule for the problem (lines 17-18). Finally, the objective value \(obj\) is returned (line 19), which is the upper bound \(C\) of \(A\). Because our heuristic algorithm is not an optimal algorithm, for some solvable problems, it cannot find feasible solutions. Therefore, when our heuristic algorithm cannot return the upper bound, we calculate one:  
\[C=\sum_{\forall m\in[1,M)}\,(w^{m}\times|V^{m}|). \tag{11}\]Equation (11) means that all packets are covered except those with the maximum number of transmissions. This is the worst case. The value of \(A\) must not be greater than Equation (11). Therefore, the worst case \(C\) must be the searching boundary of \(A\). Based on the above theorems and algorithm, we can obtain the lower bound \(B\) and upper bound \(C\) of \(A\). However, although the values of \(A\) can be ordered in the range \([B,C]\), the satisfiability of SMT(\(A\)) is not monotonic with respect to the order of \(A\) (Theorem 3). Therefore, to avoid missing the minimum value of \(A\), we must check the values one by one from \(B\) to \(C\) until a value satisfies SMT(\(A\)). The value is the objective value of our problem. Since \(B\) is a tight bound, the objective value can be found after a few verifications. Even so, the solution time of the SMT-based method is still less than that of the OMT method. The comparison between them is shown in Section 6. **Theorem 3** (Non-monotonicity). : _The satisfiability of SMT(\(A\)) is not monotonic with respect to the order of \(A\)._  
Proof. : If SMT(\(n\)) \((n>0)\) is satisfiable, SMT(\(n-1\)) and SMT(\(n+1\)) may or may not be satisfiable. We list four cases to illustrate that there can be any relationship among SMT(\(n-1\)), SMT(\(n\)), and SMT(\(n+1\)). (1) SMT(\(n\)) is satisfiable, and SMT(\(n+1\)) is satisfiable.