This paper presents an iterative approximation re nement, 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 re ned by decomposition, a re nement 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 re ning strategies, e.g., the result of interval arithmetic re nes both test data generation and next re nements, and the result of testing re nes next re nements. 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 clauses for heuristics isHalt clauses for refinement SAT solver
Result (UNSAT/unknown)
A SAT solution M clauses for conflict Refinement Over-approximation O.T-UNSAT theory