raSAT: SMT for Polynomial Inequality
Van Khanh To, Mizuhito Ogawa · Institutional Repositories DataBase (IRDB) · 2013
This paper presents an iterative approximation refinement, called raSAT loop, which solves polynomial inequality constraints on real numbers. The approximation scheme consists of interval arithmetic (over-approximation, aiming to decide unsatisfiability) and testing (underapproximation, aiming to decide satisfiability). If both of them fail to decide, input intervals are refined by decomposition. raSAT loop is implemented as an SMT raSAT with miniSAT 2.2 as a backend SAT solver. Experiments including simple benchmarks for estimating effects of input measures (i.e., degrees, number of variables, and number of constraints) and QF_NRA benchmarks from SMT-LIB show that raSAT is comparable to Z3 4.3, and sometimes outperforms, especially with high degree of polynomials.