The satisfiability problem modulo the nonlinear real arithmetic (NRA) theory serves as the foundation for a wide range of important applications, such as model checking, program analysis, and software testing. However, due to the high computational complexity, developing efficient solving algorithms for this problem has consistently presented a substantial challenge. We present a hybrid SMT(NRA) solver, called NRAgo, which combines the efficiency of gradient-based optimization method with the completeness of algebraic solving algorithm. With our approach, the practical performance on many satisfiable instances is substantially improved. The experimental evaluation shows that NRAgo achieves remarkable acceleration effects on a set of challenging SMT(NRA) benchmarks that are hard to solve for state-of-the-art SMT solvers.

Minghao Liu

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Kunhang Lv

Institute of Software, Chinese Academy of Sciences

China

Pei Huang

Stanford University

United States

Rui Han

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Fuqi Jia

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Yu Zhang

Institute of Software, Chinese Academy of Sciences

Feifei Ma

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China

Jian Zhang

Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences

China