+********************************************************************** * * * Einladung * * * * Informatik-Oberseminar * * * +**********************************************************************
Zeit: Freitag, 14. Dezember 2018, 13:00 Uhr Ort: Gebäude E3, Seminarraum 9222, Ahornstr. 55
Referent: Ulrich Loup Theory of Hybrid Systems Informatik 2
Thema: On Solving Real-algebraic Formulas in a Satisfiability-modulo-theories Framework
Abstract:
Quantifier-free real-algebraic formulas are Boolean combinations of polynomial equations and inequalities over the domain of the real numbers. Coming with a strong expressiveness and a still decidable satisfiability problem, real- algebraic formulas are a precious modeling language in many academic, industrial and commercial areas. However, only some classes of real-algebraic formulas allow an efficient solving in practice. For instance, conjunctions of linear real-algebraic constraints can be solved with the very successful simplex method.
The general quantifier-free real-algebraic satisfiability problem, however, has a worst-case time complexity bound which is exponential in the number of input variables. Methods solving this general problem directly are often inefficient in practice. The very popular cylindrical algebraic decomposition (CAD) method has a doubly-exponential complexity bound in the number of input variables for its search space.
This thesis tackles the solving of general quantifier-free real-algebraic formulas with a combination of different methods in a satisfiability-modulo- theories (SMT) framework: A SAT solver computes partial assignments for the Boolean structure of the real-algebraic formula and real-algebraic solvers check these assignments for consistency in the real domain. If the assignment is infeasible in the real domain, the SAT solver would profit from a small - preferably minimal - reason for this conflict in terms of a subset of the constraints corresponding to the conflicting assignment.
In this talk, I focus on two real-algebraic solvers in our SMT-solving framework SMT-RAT, which are major contributions of my thesis. The first solver is an implementation of the CAD method specialized for an efficient embedding into an SMT solver. In particular, the CAD method is extended by the ability to solve incrementally, i.e. reuse pre-computed results, to backtrack and to compute minimal reasons. Moreover, bounds to the variables are used to prune the CAD search space, especially when combining the method with interval-arithmetic techniques.
The second solver uses an extension of Buchberger's algorithm in order to compute a Gröbner basis. The solver supports incremental solving, backtracking and minimal reasons for some unsatisfiable cases, as well. We extended the method so that the solver can also be used in order to simplify formulas for other real-algebraic solvers in the SMT-solving framework. As a main part, my thesis comprises an evaluation of the two solvers in the SMT-RAT framework. In particular, the effects of combining the CAD method with a Gröbner-bases solver in an SMT framework are investigated.
In my talk, some experimental results of this evaluation are shown, too.