raSAT: SMT for Polynomial Inequality
                   (extended abstract)
         To Van Khanh1 , Vu Xuan Tung2 , and Mizuhito Ogawa2
                          1
                        University of Engineering and Technology,
                          Vietnam National University, Hanoi
                                 khanhtv@vnu.edu.vn
                  2
                    Japan Advanced Institute of Science and Technology
                      tungvx@jaist.ac.jp, mizuhito@jaist.ac.jp

                                                    Abstract
    This paper presents an iterative approximation refinement, called raSATloop, which
solves a system of polynomial inequalities on real numbers. The approximation scheme
consists of interval arithmetic (over-approximation, aiming to decide UNSAT) and testing
(under-approximation, aiming to decide SAT). If both of them fail to decide, input intervals
are refined by decomposition, a refinement step in raSATloop.
    The SMT solver raSAT implements the raSATloop, on top of the miniSAT 2.2, with
backend theories in Ocaml. The raSATloop is not only a simple framework, but also allows
us to design mutually refining strategies, e.g., the result of interval arithmetic refines
both test data generation and next refinements, and the result of testing refines next
refinements. We discuss three strategy design choices: dependency to set priority among
atomic polynomial constraints, sensitivity to set priority among variables, and UNSAT core
for reducing learned clauses and incremental UNSAT detection.


                                                 A target constraint F



                  Termination                                            UNSAT         Result
                   Heuristics
                                                     SAT solver                   (UNSAT/unknown)
                                   clauses for
                                    heuristics


                 isHalt                                                      clauses for
                              clauses for                     A SAT            conflict
                              refinement                    solution M




                                             Over-approximation             O.T-UNSAT        Theory
                Refinement                                                                 Propagation
                                                   theory



                                                                                        O.T-VALID
                              U.T-UNSAT                      O.T-SAT




                                             Under-approximation U.T-SAT                    Result
                                                   theory                                   (SAT)




                                            Figure 1: raSATloop