NRAgo: Solving SMT(NRA) Formulas with Gradient-Based Optimization
Abstract
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.
BibTeX
@inproceedings{Liu-al:ASE23,
author = {Minghao Liu and
Kunhang Lv and
Pei Huang and
Rui Han and
Fuqi Jia and
Yu Zhang and
Feifei Ma and
Jian Zhang},
title = {{NRAgo:} Solving {SMT(NRA)} Formulas with {Gradient-Based} Optimization},
booktitle = {ASE},
pages = {2046--2049},
publisher = {{IEEE}},
year = {2023},
}