SMT-RAT: An SMT-Compliant Non-linear Real Arithmetic Toolbox

Speaker

Ulrich Loup
Title SMT-RAT: An SMT-Compliant Non-linear Real Arithmetic Toolbox
When 05.09.2012, 10.00
Where Room 5052
Abstract In Satisfiability-Modulo-Theories (SMT) solving, a SAT solver works hand in hand with solvers for conjunctions of constraints from a first-order theory, more expressive than propositional logic. We consider the theory of the reals with addition and multiplication, called non-linear real arithmetic (NRA) in the SMT jargon. Solving for this theory is very hard and requires the combination of a number of different solving techniques in order to be feasible in practice. Already small examples show that the decision as to which technique is best for solving a particular instance should in general not be taken by a fixed strategy. Our goal is to involve the user in this decision.

We present SMT-RAT, a modular C++ toolbox for the development of a theory solver for NRA, compliant with the SMT framework. The toolbox offers modules implementing different NRA solving techniques, which the user can arrange in strategies. Using OpenSMT, an open-source SMT solver, we were able to achieve preliminary results on the effects of different strategies. We also compared our solver with other state-of-the-art SMT solvers for NRA.
Slides