Computer Science Graduate Seminar

Thursday, March 12, 2020, 10:45am

Cylindrical Algebraic Decomposition for Nonlinear Arithmetic Problems

  • Location: Room 9222, E3 building, Ahornstr. 55
  • Speaker: Gereon Kremer M.Sc. (Theory of Hybrid Systems)

 

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.

 

The computer science lecturers invite interested people to join.