This page has been moved to

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



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