标题： 通过MCSAT集成改进SMT-NRA中的局部搜索 显示英文标题

标题： Advancing Local Search in SMT-NRA with MCSAT Integration

摘要： 在本文中，我们推进了满足非线性实数算术理论的可满足性问题（SMT-NRA）的局部搜索。 首先，我们引入了一种二维单元跳跃移动，称为\emph{$2d$-单元跳跃}，这是 SMT-NRA 局部搜索方法中的关键操作单元跳跃的推广。 然后，我们提出了一种扩展的局部搜索框架，命名为\emph{$2d$-LS}（遵循 SMT-NRA 的局部搜索框架 LS），将模型构建可满足性演算（MCSAT）框架集成以提高搜索效率。 为了进一步提高 MCSAT 的效率，我们实现了一种最近提出的称为\emph{样本单元投影算子}的技术，该技术非常适合实数域中的 CDCL 风格搜索，并有助于引导搜索远离冲突状态。 最后，我们设计了一个结合 MCSAT、$2d$-LS 和 OpenCAD 的 SMT-NRA 混合框架，通过信息交换提高搜索效率。 实验结果展示了局部搜索性能的提升，突显了所提出方法的有效性。 显示英文摘要

摘要： In this paper, we advance local search 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 design a hybrid framework for SMT-NRA combining 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.