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

arXiv: https://arxiv.org/abs/2507.00557 · HTML: https://mlsanity.com/paper/2507.00557/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 3 of its 33 references that are in the map.
- First posted on arXiv 1 Jul 2025.

## Builds on (most cited first, 3 of 3)

- [Local Search for Solving Satisfiability of Polynomial Formulas](https://mlsanity.com/paper/2303.09072/) (2023)
- [Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection](https://mlsanity.com/paper/2003.00409/) (2020)
- [Local Search For SMT On Linear and Multilinear Real Arithmetic](https://mlsanity.com/paper/2303.06676/) (2023)

## Abstract (arXiv)

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 move, called 2d-cell-jump, generalizing the key operation, cell-jump, of the local search method for SMT-NRA. Then, we propose an extended local search framework, named 2d-LS (following the local search framework, LS, for SMT-NRA), integrating the model constructing satisfiability calculus (MCSAT) framework to improve search efficiency. To further improve the efficiency of MCSAT, we implement a recently proposed technique called sample-cell projection operator for MCSAT, which is well suited for CDCL-style search in the real domain and helps guide the search away from conflicting states. Finally, we present a hybrid framework for SMT-NRA integrating MCSAT, 2d-LS and OpenCAD, to improve search efficiency through information exchange. The experimental results demonstrate improvements in local search performance, highlighting the effectiveness of the proposed methods.