Satisfiability Modulo Theories (SMT) has significant application in various domains. In this paper, we focus on quantifier-free Satisfiablity Modulo Real Arithmetic, referred to as SMT(RA), including both linear and non-linear real arithmetic theories. As for non-linear real arithmetic theory, we focus on one of its important fragments where the atomic constraints are multi-linear. We propose the first local search algorithm for SMT(RA), called LocalSMT(RA), based on two novel ideas. First, an interval-based operator is proposed to cooperate with the traditional local search operator by considering the interval information. Moreover, we propose a tie-breaking mechanism to further evaluate the operations when the operations are indistinguishable according to the score function. Experiments are conducted to evaluate LocalSMT(RA) on benchmarks from SMT-LIB. The results show that LocalSMT(RA) is competitive with the state-of-the-art SMT solvers, and performs particularly well on multi-linear instances.

翻译：可满足性模理论（SMT）在多个领域具有重要应用。本文聚焦于无量词版本的可满足性模实数算术（简称SMT(RA)），涵盖线性与非线性实数算术理论。针对非线性实数算术理论，我们关注其原子约束为多重线性的重要子片段。基于两项创新思想，我们提出了首个面向SMT(RA)的局部搜索算法LocalSMT(RA)。首先，提出一种基于区间的算子，通过利用区间信息与传统局部搜索算子协同操作。其次，设计了一种破平机制，当各操作在评分函数下无法区分时，对其进行进一步评估。在SMT-LIB基准测试上的实验结果表明，LocalSMT(RA)与现有最优SMT求解器具有竞争力，尤其在多重线性实例上表现优异。