# Improving Symbolic System-Level Synthesis by Solver Coordination and Domain-Specific Heuristics
## 8 Experimental Results
### Experimental Setup
Once a scheduling problem is defined, different instances of the solver \(\mathtt{yices}\) are started in parallel using the algorithms Floyd-Warshall (command line parameter -\(\mathtt{arith-solver=floyd-warshall}\)) and the simplex algorithm (command line parameter -\(\mathtt{arith-solver=simplex}\)) for the logic quantifier-free integer difference logic (\(\mathtt{GF\_IDL}\)). Furthermore, the results of [43] encouraged us to also start one instance of \(\mathtt{yices}\) in quantifier-free linear integer arithmetic (\(\mathtt{GF\_LIA}\)) in default configuration. However, for our test instance, the linear integer arithmetic configuration does not show significant improvements compared to the integer difference logic of \(\mathtt{yices}\) as suggested in [43]. Along with the different configuration of the \(\mathtt{yices}\) solver, our portfolio approach also starts an instance of the Z3 solver in default configuration in logic \(\mathtt{GF\_IDL}\). Furthermore, we also try to decide arising scheduling problems faster by incorporating an \(\mathtt{UNSAT}\)-hypothesis approach. Here, in every scheduling problem the constraints associated with scheduling computational tasks or messages on resources are incrementally added as long as the preceding problem was decided as feasible. The benefit of this iterative solving is that already a rather small (sub-)problem might be decided as infeasible within a shorter amount of time. Including this technique also resembles to some extent other approaches that try to decide on _incomplete models_ (partial assignments on binding and routing variables), e.g., [9; 10], but in our work this is more adapted to be consistent with the additions we made, e.g., the set-based deletion filter (cf. Section 7). Subsequently, if a problem is decided unsatisfiable in the iterations within the \(\mathtt{UNSAT}\)-hypothesis, the unsatisfiable core extraction starts on a smaller problem instance. Similar to the portfolio solving approach for the background theory as described above, we invoke four different solver configuration for each scheduling problem in the \(\mathtt{UNSAT}\)-hypothesis  
Independent of which hypothesis was used to decide a scheduling problem instance, once any of the differently configured background theory solvers reached a point where it determined a scheduling problem as unsatisfiable or satisfiable, this result is used (including logging the respective runtime returned by the solver) and all other solver instances running in parallel are stopped. Regarding the hierarchical scheduling scheme (cf. Section 7), at each stage we decide the feasibility of sub-problems iteratively. Once we found that a scheduling problem is not feasible, the associated MUC is extracted and immediately returned to the logic solver as explained in Section 7. Thus, no further sub-problems in a stage are tried to be solved once an infeasible solution was found. Since our _coordinated_ approach is non-deterministic, each instance is always run 5 times (what we also do for the _classical_ approach). This non-determinism is due to the fact that we ultimately use the timer of the operation system to interrupt the lexicographical optimization in the answer set solver in the coordinated approach. Since the interruption by the timer might only jitter minimally, this is enough that the answer set solver might advance only a little bit in its solving process and other solutions are passed to the analysis in the background theory. By running each instance 5 times we gather statistics over the non-deterministic processes. The time limit for each run was always set to 3600 s in order to derive a feasible system synthesis.