raSAT: an SMT solver for Polynomial Constraints
raSAT brief description
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 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 Propagation (ICP), similar to
raSAT prepares various Interval Arithmetic as an over-approximation theory, which are mostly
Affine Intervals. It also prepares Testing (with several strategies) as an under-approximation theory.
raSAT accepts problems in SMT-LIB format (.smt2)
- Version 0.4 is a parallel combination of different heuristics, June 2016.
- Version 0.3, released on 2 Feb 2016
- Version 0.2, released on 28 May 2015
- Version 0.1, released on 22 Jan 2014
Vu Xuan Tung, To Van Khanh, Mizuhito Ogawa. raSAT: an SMT Solver for Polynomial Constraints. International Joint Conference on Automated Reasoning 2016. IJCAR 2016: Volume 9706 Pages 228-237. [PDF][Link].
Vu Xuan Tung, To Van Khanh, and Mizuhito Ogawa. raSAT 0.2 for SMT-COMP 2015. The 10th International Satisfiability Modulo Theories Competition. SMT-COMP 2015.
To Van Khanh, Xuan-Tung Vu, Mizuhito Ogawa. raSAT: SMT for Polynomial Inequality. The 12th International Workshop on Satisfiability Modulo Theories. SMT Workshop 2014: 67.
To Van Khanh, Mizuhito Ogawa,
raSAT: SMT for polynomial inequality,
JAIST Research Report IS-RR-2013-003.
Khanh, T.V., Ogawa, M.: SMT for polynomial constraints on real numbers.
Electronic Notes in Theoretical Computer Science 289(0), 27 − 40 (2012), third
Workshop on Tools for Automatic Program Analysis (TAPAS 2012).
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 @.