# Improving Symbolic System-Level Synthesis by Solver Coordination and Domain-Specific Heuristics
## 2 Coordinated SMT-Based Synthesis Approach: Motivation & Detailed Overview
### (Classical) SMT-Based System Synthesis
In Section 7 we will introduce the hierarchical scheduling stages in detail. If the background theory solver proves that a scheduling (sub-)problem cannot be solved, a subsequent conflict analysis (red box in Figure 2) is started. Here, we also benefit from the hierarchical scheduling scheme as it usually speeds up the conflict analysis since smaller sub-problems have to be analyzed. During conflict analysis, an _minimal unsatisfiable core_ (or _justification_, _unsatisfiable core_ or _irreducible inconsistent subset_) [15] is derived why no time-triggered schedule exists. For example, assume a schedule cannot be derived for a PE with five computational tasks bound to it. However, the minimal unsatisfiable core for the conflict could be that only two of these tasks prevent scheduling due to their timing parameters. All combinations including both two tasks are thus infeasible. And this is also true for bindings, which have not been seen up to this point. Related work [6] has shown that deriving a minimal unsatisfiable cores in a conflict analysis can significantly speed up the scalability of symbolic system synthesis as it can enable an extensive pruning of the logic solver's search space. Revisiting our previous example, all solutions where the two conflicting computational tasks are bound to the same PE will not result in a feasible implementation and should therefore be excluded in the search space of the logic solver. Thus, a feedback to the logic solver is generated that restricts the subsequent binding and routing solutions of the logic solver (purple box in Figure 2). Here, as mentioned earlier, the indicator variables are used to constrain the search space by adding so-called integrity constraints to the set of rules of the logic solver (see Section 5). All following binding and routing implementation solution candidates will avoid all conflicts from the background theory that have been learned so far. The iterative coupling between logic solver and \(\mathcal{T}\)-solver stops with a successfully hierarchical scheduling or if the logic solver returns the result UNSAT (unsatisfiable). In the latter case the SMT-based synthesis approach proved that there exists no feasible implementation with respect to the system's specification. Regarding the complexity of the system specifications that the _classical_ approach is able to synthesize, this approach can face serious applicability issues, as we will see later within our experimental section (Section 8). This is due to the often very complex and time consuming time-triggered scheduling analysis within the background theory solver. The upper timeline in Figure 3 illustrates the observation that is usually made. Here, the logic solver is able to compute a binding and routing solution within a very short amount of time (blue box in Figure 3), often even within milliseconds. However, the subsequent scheduling analysis and conflict analysis (orange and red boxes in Figure 3) are very time consuming and several magnitudes higher than the time spent in the logic solver. Hence, the necessary feedback from the \(\mathcal{T}\)-solver to the logic solver cannot be derived within a reasonable amount of time which can ultimately limit the applicability of _classical_ SMT-based system synthesis. Usually, the _classical_ approach is stopped after a certain timeout without providing a solution to the synthesis problem (see experiments in Section 8). As a remedy, we propose a _coordinated_ SMT-based synthesis approach with the logic solver computing a binding and routing solution such that the \(\mathcal{T}\)-solver is able to decide feasibility within a reasonable amount of time.