# Improving Symbolic System-Level Synthesis by Solver Coordination and Domain-Specific Heuristics
## 7 Coupling ASP and Background Theory  
Given a binding \(\mathbf{B}\) and routing \(\mathbf{R}_{\text{route}}^{bkts}\) derived by the logic solver, a scheduling \(\mathbf{S}\) can be computed. However, in a first iteration of our SMT-based approach, two unfortunate observations can be made. First, deciding whether a binding and routing solution is schedulable takes considerable time, even if one uses our proposed _coordinated_ approach. Second, early binding and routing solutions of the logic solver often cannot be scheduled. A reason for the first observation is that in common approaches all computational tasks and packets are scheduled at once on the resources of the hardware platform. Thus, this results in a potentially large scheduling problem and usually long runtimes of the background theory in order to decide schedulability. Though, deciding feasibility of solution candidates in the background theory in a fast manner is a key ingredient for the performance of the whole synthesis approach. As a remedy, we address the first observation by introducing a hierarchical scheduling scheme suiting our system model based on modifications of the scheme introduced in [7] (see Figure 5). Instead of analyzing the whole system at once, we step through the stages of our scheme and decide on essential sub-problems:  
1. Schedule computational tasks on each tile independently (TS),
2. Schedule computational tasks on each tile with the incoming and outgoing packets of the tile independently (CS),
3. Schedule clusters of independent applications independently (AS). Deciding the scheduling feasibility of the sub-problems usually takes considerably less time compared to deciding the complete system. Furthermore, if, e.g., already the computational tasks on one tile cannot be scheduled, scheduling the whole system is also not possible and further effort in stepping through the hierarchical scheduling scheme can be saved. If all sub-problems of one stage are feasible, the problems of the subsequent stage in our hierarchical scheduling scheme are analyzed. Ultimately, if all sub-problems of the final stage can be solved, a feasible implementation is found. In contrast, if a sub-problem is infeasible, we are again in the situation of the second observation as stated above. The second observation is addressed by providing accurate feedback from the background theory to the answer set solver as common in SMT-based approaches. Here, the feedback should at least prohibit that the exact same infeasible binding and routing is not proposed a second time. From related work, e.g., [6], we know that the scalability of symbolic system synthesis can further be significantly increased by deriving a minimal unsatisfiable core (MUC), i.e., a minimal reason why a schedule cannot be derived. Hence, if the MUC is propagated back to the answer set solver, often considerable amounts of infeasible design space can be pruned. Once a sub-problem in the stage (TS) is infeasible, we apply a set-based deletion filter algorithm (see Algorithm 1) to deduce one MUC, similar to [7]. Let \(\mathbf{T}_{\perp}^{\dagger}\) be the set of all computational tasks on one tile \(r\in\mathbf{R}_{t}\) that form the infeasible set of constraints \(\mathbf{C}_{\perp}\). In contrast to deletion filters known form the related work, e.g., [38], the set-based deletion filter requires only \(|\mathbf{T}_{\perp}^{\dagger}|\) instead of \(|\mathbf{C}_{\perp}|\) iterations. Thus, deriving a MUC can  
Figure 5: Detailed overview of the flow within the coupling of the answer set solver and the background theory solver. be considerably faster since the number of tasks is noticeably lower than the number of constraints. Note that using the set-based deletion filter does not have any downsides in terms of expressiveness of the MUC since the logic solver does not relate to constraints \(c\in\mathbf{C}_{\perp}\) that are used in the \(\mathcal{T}\)-solver. For example, in the case of scheduling computational tasks on tiles, the logic solver can only relate to entities of computational tasks.