raSAT
| swMATH ID: | 15206 |
| Software Authors: | Khanh, T. V.; Ogawa, M. |
| Description: | 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. |
| Homepage: | http://www.jaist.ac.jp/~mizuhito/tools/rasat.html |
| Related Software: | SMT-RAT; z3; CVC4; Yices; MathSAT5; SMT-LIB; CoCoALib; MiniSat; dReal; veriT; cvc5; GitHub; Boogie; Coq; Lingeling; Treengeling; Plingeling; QEPCAD; iRRAM; StarExec |
| Cited in: | 14 Documents |
all
top 5
Cited by 36 Authors
Cited in 5 Serials
all
top 5
