混合 SMT-NRA 求解器：融合 2D-cell-jump 局部搜索、MCSAT 与 OpenCAD
A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD
AI 导读
论文提出一个 SMT-NRA（非线性实数可满足性模理论）混合求解框架，将局部搜索、MCSAT 与 OpenCAD 整合，通过信息交换提升搜索效率。作者首先提出 2D-cell-jump 操作，将原有沿给定直线更新赋值的 cell-jump 推广到任意选定平面上的搜索，并构建扩展局部搜索框架 2D-LS。实验结果显示局部搜索性能得到改进，验证了方法的有效性。
正文 · 原文
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.
| Comments: | Camera-ready version for SETTA 2026 |
| Subjects: | Artificial Intelligence (cs.AI); Logic in Computer Science (cs.LO); Symbolic Computation (cs.SC) |
| Cite as: | arXiv:2507.00557 [cs.AI] |
| (or arXiv:2507.00557v3 [cs.AI] for this version) | |
| https://doi.org/10.48550/arXiv.2507.00557 arXiv-issued DOI via DataCite |
Submission history
From: Tianyi Ding [view email]
[v1]
Tue, 1 Jul 2025 08:27:29 UTC (3,728 KB)
[v2]
Fri, 11 Jul 2025 15:40:25 UTC (3,575 KB)
[v3]
Fri, 30 Oct 2026 14:03:11 UTC (5,187 KB)
来源：arXiv cs.AI · arxiv.org