提出融合多种技术的非线性实数逻辑求解框架，提升求解效率。
A Hybrid SMT-NRA Solver: Integrating 2D Cell-Jump-Based Local Search, MCSAT and OpenCAD
- 引入二维单元跳跃搜索机制，增强局部搜索能力。
- 结合MCSAT与样本单元投影，有效避免冲突状态。
- 适合需要高效求解非线性实数约束的科研与工程场景。
本文提出一种求解非线性实数算术可满足性问题（SMT-NRA）的混合框架。首先，提出一种二维单元跳跃操作（2d-cell-jump），推广了原有局部搜索方法中的关键操作。其次，构建扩展的局部搜索框架2d-LS，整合模型构造可满足性演算（MCSAT）以提升搜索效率。为优化MCSAT性能，引入近期提出的样本单元投影算子，该算子适用于CDCL风格的实数域搜索，有助于引导搜索避开冲突状态。最后，提出融合MCSAT、2d-LS与OpenCAD的混合求解框架，通过信息交换进一步提升效率。实验结果表明，局部搜索性能显著改善，验证了所提方法的有效性。
原文摘要 · Abstract (English)
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. Then, we propose an extended local search framework, named \emph{$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 \emph{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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。