+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +********************************************************************** Zeit: Donnerstag, 12. März 2020, 10:45 Uhr Ort: Raum 9222, Gebäude E3, Ahornstr. 55 Referent: Gereon Kremer, M.Sc. Theory of Hybrid Systems Thema: Cylindrical Algebraic Decomposition for Nonlinear Arithmetic Problems Abstract: We explore the usage of the cylindrical algebraic decomposition method for satisfiability modulo theories solving, both theoretically and experimentally. This method is commonly understood as an almost atomic procedure that gathers information about an algebraic problem and then allows to answer all kinds of questions about this algebraic problem afterwards. We essentially break up this method into smaller components that we can then process in varying order to derive the particular piece of information – whether the problem is satisfiable or unsatisfiable – allowing to avoid some amount of computations. As this method often exhibits doubly exponential running time, these savings can be very significant in practice. We then turn to an alternative approach to satisfiability modulo theories solving commonly called model-constructing satisfiability calculus. The core idea of this framework is to integrate the theory reasoning, in particular the construction of a theory model, very tightly with the Boolean reasoning. The main theory reasoning engine is again based on the cylindrical algebraic decomposition method, though we focus more on the overall framework here. Es laden ein: die Dozentinnen und Dozenten der Informatik -- Gereon Kremer Lehr- und Forschungsgebiet Theorie Hybrider Systeme RWTH Aachen Tel: +49 241 80 21243