Local search has recently been applied to SMT problems over various arithmetic theories. Among these, nonlinear real arithmetic poses special challenges due to its uncountable solution space and potential need to solve higher-degree polynomials. As a consequence, existing work on local search only considered fragments of the theory. In this work, we analyze the difficulties and propose ways to address them, resulting in an efficient search algorithm that covers the full theory of nonlinear real arithmetic. In particular, we present two algorithmic improvements: incremental computation of variable scores and temporary relaxation of equality constraints. We also discuss choice of candidate moves and a look-ahead mechanism in case when no critical moves are available. The resulting implementation is competitive on satisfiable problem instances against complete methods such as MCSAT in existing SMT solvers.

翻译：局部搜索最近被应用于各种算术理论的SMT问题中。其中，非线性实数算术因其不可数的解空间以及可能需要求解高次多项式而带来特殊挑战。因此，现有的局部搜索工作仅考虑了该理论的子片段。本文分析了这些难点并提出解决思路，从而得到一种覆盖非线性实数算术完整理论的高效搜索算法。具体而言，我们提出了两项算法改进：变量得分的增量计算与等式约束的临时松弛。我们还讨论了候选移动的选择，以及在无关键移动可用时的前瞻机制。实验表明，所实现算法在可满足问题实例上的性能与现有SMT求解器中的MCSAT等完备方法具有竞争力。