Satisfiability Modulo Theories (SMT) has significant application in various domains. In this paper, we focus on 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 fragment where the atomic constraints are multilinear. We proposed the first local search algorithm for SMT(RA), called LS-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 LS-RA on benchmarks from SMT-LIB. The results show that LS-RA is competitive with the state-of-the-art SMT solvers, and performs particularly well on multilinear instances.

翻译：可满足性模理论（SMT）在多个领域具有重要应用。本文聚焦于实数算术可满足性模理论（SMT(RA)），涵盖线性和非线性实数算术理论。针对非线性实数算术理论，我们重点关注其重要子片段——原子约束为多线性的情形。我们提出了首个面向SMT(RA)的局部搜索算法LS-RA，该算法基于两项创新思想：首先，提出一种基于区间的算子，通过融入区间信息来协同传统局部搜索算子；其次，设计了一种打破平局机制，用于在根据评分函数无法区分操作时进行进一步评估。在SMT-LIB基准测试上的实验结果表明，LS-RA与当前最先进的SMT求解器性能相当，并在多线性实例上表现尤为突出。