This page has been moved to http://www.jaist.ac.jp/~s1520002/raSAT.

raSAT: an SMT solver for Polynomial Constraints

raSAT brief description

raSAT is an SMT to solve problems in QF_NRA(QF_NIA) category, i.e., Quantifier-Free Non-linear constraint with Real (Integer) Arithmetic. It combines miniSAT 2.2 and background theories, which are various Interval Arithmetics. Main features are,

raSAT download

raSAT history

Reference

Contact

Questions and comments to To Van Khanh (UET/VNU-HN, tovankhanh"at"gmail.com) and/or Mizuhito Ogawa (JAIST, mizuhito"at"jaist.ac.jp) and/or Vu Xuan Tung (JAIST, tungvx"at"jaist.ac.jp) - please replace "at" with @.