Solving SMT over Non-linear Real Arithmetic via Numerical Sampling and Symbolic Verification

Popular SMT solvers have achieved great success in tackling Nonlinear Real Arithmetic (NRA) problems, but they struggle when dealing with literals involving highly nonlinear polynomials. Current symbolic-numerical algorithms can efficiently handle the conjunction of highly nonlinear literals but are limited in addressing complex logical structures in satisfiability problems. This paper proposes a new algorithm for SMT(NRA), providing an efficient solution to satisfiability problems with highly nonlinear literals. When given an NRA formula, the new algorithm employs a random sampling algorithm first to obtain a floating-point sample that approximates formula satisfaction. Then, based on this sample, the formula is simplified according to some strategies. We apply a DPLL(T)-based process to all equalities in the formula, decomposing them into several groups of equalities. A fast symbolic algorithm is then used to obtain symbolic samples from the equality sets and verify whether the samples also satisfy the inequalities. It is important to note that we adopt a sampling and rapid verification approach instead of the sampling and conflict analysis steps in some complete algorithms. Consequently, if our algorithm fails to verify the satisfiability, it terminates and returns ‘unknown’. We validated the effectiveness of our algorithm on instances from SMTLIB and the literature. The results indicate that our algorithm exhibits significant advantages on SMT(NRA) formulas with high-degree polynomials, and thus can be a good complement to popular SMT solvers as well as other symbolic-numerical algorithms.