Satisfiability Modulo Theories (SMT) refers to the problem of deciding the satisfiability of a formula with respect to certain background first order theories. In this paper, we focus on Satisfiablity Modulo Integer Arithmetic, which is referred to as SMT(IA), including both linear and non-linear integer arithmetic theories. Dominant approaches to SMT rely on calling a CDCL-based SAT solver, either in a lazy or eager favor. Local search, a competitive approach to solving combinatorial problems including SAT, however, has not been well studied for SMT. We develop the first local search algorithm for SMT(IA) by directly operating on variables, breaking through the traditional framework. We propose a local search framework by considering the distinctions between Boolean and integer variables. Moreover, we design a novel operator and scoring functions tailored for integer arithmetic, as well as a two-level operation selection heuristic. Putting these together, we develop a local search SMT(IA) solver called LS-IA. Experiments are carried out to evaluate LS-IA on benchmarks from SMTLIB. The results show that LS-IA is competitive and complementary with state-of-the-art SMT solvers, and performs particularly well on those formulae with only integer variables. A simple sequential portfolio with Z3 improves the state-of-the-art on satisfiable benchmark sets from SMT-LIB.

翻译：可满足性模理论（SMT）是指在特定背景一阶理论下判定公式可满足性的问题。本文聚焦于整数算术的可满足性模理论（SMT(IA)），涵盖线性和非线性整数算术理论。主流SMT方法依赖调用基于CDCL的SAT求解器（采用惰性或积极策略）。然而，作为组合问题（包括SAT）求解的竞争性方法，局部搜索在SMT领域尚未得到充分研究。我们通过直接操作变量，突破传统框架，首次提出针对SMT(IA)的局部搜索算法。通过区分布尔变量与整数变量的特性，我们构建了局部搜索框架。同时，针对整数算术设计了新型算子与评分函数，以及两级操作选择启发式策略。综合上述方法，我们开发了名为LS-IA的局部搜索SMT(IA)求解器。基于SMTLIB基准集的实验表明，LS-IA与现有最优SMT求解器相比具有竞争力和互补性，尤其擅长处理仅含整数变量的公式。与Z3组合的简单顺序集成方法，在SMT-LIB的可满足基准集上提升了现有最优性能。