A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD
· arxiv.org · popularity 6/100 · 0 similar stories today · Business Strategy & Management (Business & Finance)
Read the original at arxiv.org →
Summary
arXiv:2507.00557v3 Announce Type: replace Abstract: 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 \emph{2D-cell-jump}, generalizing the key operation, cell-jump, of the local search method for SMT-NRA. In contrast to the existing cell-jump, which updates assignments exclusively along a given line, the 2D-cell-jump enables search over an arbitrarily selected plane. Then, we propose an extended local search framework, named \emph{2D-LS} (following the existing local search framework, LS, for SMT-NRA). Finally, we present a hybrid framework for SMT-NRA integrating 2D-LS, MCSAT 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.
Found in: ArXiv CS.AI. Rating basis: single outlet; outlet tier 2 (unlisted); 1 feeds; feed position 188.