raSAT: SMT solver for Polynomial Constraints on Real numbers. raSAT is an SMT to solve problems in QF_NRA category, i.e., bounded quantification on conjunction of polynomial inequalities. It combines miniSAT 2.2 and background theories, which are various interval arithmetics. Main features are: raSAT applies raSAT loop, which applies over/under approximation theories. An over-approximation theory detects UNSAT, and an under-approximation theory detects SAT. If neither holds, raSAT loop refines bounded quantification by interval decompositions. raSAT is based on an interval constraint solving, similar to HySAT. raSAT prepares various interval arithmetics as over-approximation theories, which are mostly Affine intervals. It also prepares testing (with several strategies) as under-approximation theories. raSAT installation is confirmed on Win7, Win8 / cygwin 64bit (not 32bit), and linux. raSAT accepts inequality problems in SMT-LIB format (.smt2) (including the use of ”>=” and ”<=” in formulae, but not $=$), which is confirmed on meta-tarski, hong, zankl benchmarks.
Keywords for this software
References in zbMATH (referenced in 5 articles )
Showing results 1 to 5 of 5.
- Tung, Vu Xuan; Khanh, To Van; Ogawa, Mizuhito: raSAT: an SMT solver for polynomial constraints (2017)
- Brauße, Franz; Korovina, Margarita; Müller, Norbert: Using Taylor models in exact real arithmetic (2016)
- Kremer, Gereon; Corzilius, Florian; Ábrahám, Erika: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic (2016)
- Maréchal, Alexandre; Fouilhé, Alexis; King, Tim; Monniaux, David; Périn, Michael: Polyhedral approximation of multivariate polynomials using handelman’s theorem (2016)
- Tung, Vu Xuan; Van Khanh, To; Ogawa, Mizuhito: raSAT: an SMT solver for polynomial constraints (2016)