TY - GEN
T1 - NRAgo
T2 - 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023
AU - Liu, Minghao
AU - Lv, Kunhang
AU - Huang, Pei
AU - Han, Rui
AU - Jia, Fuqi
AU - Zhang, Yu
AU - Ma, Feifei
AU - Zhang, Jian
N1 - Publisher Copyright:
© 2023 IEEE.
PY - 2023
Y1 - 2023
N2 - 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.
AB - 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.
KW - gradient-based optimization
KW - nonlinear real arithmetic
KW - satisfiability modulo theories
UR - http://www.scopus.com/inward/record.url?scp=85179000870&partnerID=8YFLogxK
U2 - 10.1109/ASE56229.2023.00013
DO - 10.1109/ASE56229.2023.00013
M3 - Conference contribution
AN - SCOPUS:85179000870
T3 - Proceedings - 2023 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023
SP - 2046
EP - 2049
BT - Proceedings - 2023 38th IEEE/ACM International Conference on Automated Software Engineering, ASE 2023
PB - Institute of Electrical and Electronics Engineers Inc.
Y2 - 11 September 2023 through 15 September 2023
ER -
