Solving SMT over Non-linear Real Arithmetic via Numerical Sampling and Symbolic Verification. - Xinpeng Ni; Yulun Wu; Bican Xia (SETTA, 2023)

Local Search for Checking Satisfiability of Formulas with Trigonometric Functions. - Xinpeng Ni; Bican Xia; Tianqi Zhao (ATVA (2), 2024)

A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD. - Tianyi Ding; Haokun Li; Xinpeng Ni; Bican Xia; Tianqi Zhao (CoRR, 2025)