activity
20182025
most citedIsolating Bounded and Unbounded Real Roots of a Mixed Trigonometric-Polynomial

1 citations · 1 across the 8 of their papers we have counts for

collaborators
Showing 2025Show all

1 paper · 1 filter

cs.AI2025

A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD

Tianyi Ding, Haokun Li, Xinpeng Ni +2

In this paper, we propose a hybrid framework for Satisfiability Modulo the Theory of Nonlinear Real Arithmetic (SMT-NRA for short). First, we introduce a two-dimensional cell-jump…