Speaker |
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. |
Slides |
Event calendar
- Subscribe to the ics feed.
Upcoming Events
- No Events