iv

Satisfiability modulo theory (SMT) solvers exist for various theories of first-order logic, whereas the theory of quantifier-free nonlinear real arithmetic (QFNRA) problems is quite unexplored. Corresponding state-of-the-art SMT solvers are still actively developed in order to achieve further efficiency for their underlying implemented methods. SMT solvers are developed towards well-known problems, but seem to be-have less sophisticated in unknown fields, especially those which have emerged through practical issues. This downside can mostly be vanished, when rear-ranging the utilization order of the used approaches. The strategy challenge proposes combinations of them, which can flexibly and easily be defined by the user in order to improve the efficiency of an SMT solver for new problem classes. The SMT toolbox for real arithmetic, short SMT-RAT, allows the creation of SMT solvers for QFNRA problems according to a user-defined strategy. This thesis introduces an improved strategy approach for this toolbox and presents a user-friendly GUI for creating them. The new approach entails the possibility for the user to intend alternative combinations of solving procedures, depending on dynamically determined conditions on the input. Furthermore, it is capable to apply these procedures even in parallel, which can be considered as a novel achievement in this field of research. iii Erklärung Hiermit versichere ich, dass ich die vorgelegte Arbeit selbstständig verfasst und noch nicht anderweitig zu Prüfungszwecken vorgelegt habe. Alle benutzten Quellen und Hilfsmittel sind angegeben, wörtliche und sinngemäße Zitate wur-den als solche gekennzeichnet