Seminar


Joint approximations for multivariate real functions

Authors: F. Brausse, M. Korovina, N. Mueller

As a generalization of the well-known NP-complete problem SAT from propositional logic, the task in SMT (Satisfiability Modulo Theories) is to determine whether certain quantifier-free formulae in first-order logic are satisfiable. Popular solvers for such problems are Z3, CVC4 or MathSAT.

We are interested in the case where the first-order logic is on real numbers. For formulae describing linear arithmetic on this set, the implementations mentioned above are quite efficient (as far as possible, having to deal with NP-completeness).

However, nonlinear arithmetic on real numbers is far harder, as general issues concerning decidability arise. In addition, techniques for the treatment of nonlinear formulae are still under development. Our approach combines ideas from CDCL-style SMT solving, computable analysis and the numerical approach of Taylor models.

In the talk we will give brief introductions into these topics and present a prototypical implementation meant for augmenting existing SMT solvers with nonlinear arithmetic.