raSAT: SMT solver for Polynomial Constraints on Real numbers

raSAT berief description

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 download

raSAT usage

raSAT history



To Van Khanh, Mizuhito Ogawa, raSAT: SMT for polynomial inequality, JAIST Research Report IS-RR-2013-003.


Questions and comments to To Van Khanh (UET/VNU-HN, tovankhanh [at] gmail.com) and/or Mizuhito Ogawa (JAIST, mizuhito [at] jaist.ac.jp). (Please replace [at] with @.)