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求解器具有竞争性与互补性，尤其擅长处理仅含整数变量的公式。通过将LS-IA与Z3简单组合为顺序集成求解器，在SMT-LIB可满足性基准集上取得了超越现有最优方法的表现。