14.8.2015 14:00 @ Other Seminars
Polynomial constraints in SMT solvers remain as a frontier, and there are many techniques, e.g., QE-CAD, virtual substitution, interval constraint propagation (ICP), bit blasting, and so on. raSAT is an ICP based SMT solver, boosted by testing to find SAT instances. We show raSAT loop for polynomial inequality and the use of intermediate value theorem for polynomial equality. By its simple nature, it is fairly easy to adapt both for real numbers and integers. This year, at our second trail to SMT-Competition, raSAT is 8th among 19 tools as overall rating, 3rd among 7 for QF_NRA category, and second among 6 for QF_NIA.
