A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra


Florian Corzilius

(Forschungsstudent, Group of Hybrid Systems)

Title A Lazy SMT-Solver for a Non-Linear Subset of Real Algebra
When 22.01.2010, 15:00
Where Lecture Room Informatik 11
Abstract We address satisfiability checking for quantifier-free formulas consisting of real algebraic constraints, i.e., polynomial constraints in several real-valued variables. This problem is indeed decidable but its complexity is in worst case doubly-exponential in the number of variables. This complexity bound is

also often met in practice, for example, in the cylindrical algebraic decomposition (CAD) method, which is implemented in computer algebra systems like Reduce.Another method, called virtual substitution method, is only single-exponential at worst, but it cannot handle complicated high-degree polynomials. As a first step to an SMT solver for solving real algebraic formulas, we modified the

virtual substitution method to fit into the SMT framework. We have an experimental test implementation, which already shows the advantages of using the SMT approach for real algebraic formulas.