# Improving Symbolic System-Level Synthesis by Solver Coordination and Domain-Specific Heuristics
## 3 Related Work  
To keep up with the increasing complexity of system specification, symbolic system synthesis approaches based on Pseudo-Boolean satisfiability (PB-SAT), e.g., [18], emerged as solutions to handle challenging system specifications where previous (meta-)heuristic approaches may fail. While these methods are able to efficiently restrict parts of the infeasible search space, they are mostly limited to linear constraints and potential binary encodings of integer domains tend to an exponential growth in variables. As a remedy, to handle non-linear functional constraints such as hard real-time timing constraints which require large numeric domains, new symbolic synthesis approaches leverage results form the area of satisfiability modulo theories (SMT) solving [15; 19]. Thereby, SMT solvers decide the satisfiability of decision problems on logical formulae and these formulae are then interpreted by background theories. In a lot of approaches the propositional part of an SMT solver is realized by a SAT solver whereas a solution with respect to the background theory is computed by a so-called \(\mathcal{T}\)-solver. As one of the first publications regarding SMT-based system synthesis, the authors in [20] make use of the SMT-solving's decomposition principle to increase the scalability. Here, the \(\mathcal{T}\)-solver solves a graph-theoretic sub-problem. In [21] latency computation is used for scheduling analysis in the \(\mathcal{T}\)-solver and the authors were able to increase performance more than an order of magnitude. Similar to our time-triggered scheduling model, the work of [22] presents an SMT-based with linear arithmetic for adding worst-case execution times within the background theory. While all the work above are SMT-based approaches, they do not incorporate the multi-hop routing and scheduling of messages. Fundamental work in SMT-based system synthesis also including the computation of multi-hop routes has been done by [PERSON] et al. [5]. The authors use Modular Performance Analysis (MPA) in combination with Real-Time Calculus [23] for timing analysis in the background theory. Furthermore, the work in [5] shows that analyzing _partial models_, i.e., checking parts of the proposed full binding and routing solution, outperforms existing approaches. The same authors further increase the performance of their approach in [6] by deducing _justifications_ (i.e., reasons why a task violates its deadline) within the background theory to prune the search space of their SAT-solver more efficiently. With these extensions, the speed-up in time to derive a feasible system synthesis in their case studies ranges from a factor of \(10\times\) up to more than \(160\times\). The approach of deducing a justification is based on analyzing the critical path set of a computational task \(t\) which violates its deadline. The critical path set is defined by all computational tasks or messages that are predecessors of task \(t\) in the same application graph. In contrast to the work at hand, the authors do not incorporate a hierarchical scheduling scheme, e.g., starting with scheduling all computational taskson the same resource independently, which could lead to smaller justifications (in terms of variables) and hence a more efficient pruning of infeasible search space. Additionally, the derived justifications are not necessarily minimal as no filter algorithm is implemented to derive _minimal unsatisfiable cores_ (see Section 7). [PERSON] et al. [10] build on the same \(\mathcal{T}\)-solver like [5; 6] but also consider delay, buffer and energy constraints of _incomplete models_. By using incomplete models, the variables of bindings and multi-hop routings proposed to the \(\mathcal{T}\)-solver are only partially assigned other than required by the system specification. As a benefit, infeasible regions of the search space can be pruned more efficiently which considerably enhances the capabilities of symbolic synthesis to prove the absence of feasible system implementations.