raSAT
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 8 articles )
Showing results 1 to 8 of 8.
Sorted by year (- Ábrahám, Erika; Davenport, James H.; England, Matthew; Kremer, Gereon: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings (2021)
- Borralleras, Cristina; Larraz, Daniel; Rodríguez-Carbonell, Enric; Oliveras, Albert; Rubio, Albert: Incomplete SMT techniques for solving non-linear formulas over the integers (2019)
- Kremer, Gereon; Ábrahám, Erika: Modular strategic SMT solving with \textbfSMT-RAT (2018)
- 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; Khanh, To Van; Ogawa, Mizuhito: raSAT: an SMT solver for polynomial constraints (2016)