论文标题
本地搜索可满足性模型整数算术理论
Local Search For Satisfiability Modulo Integer Arithmetic Theories
论文作者
论文摘要
满意度模型理论（SMT）是指确定公式对某些背景一阶理论的满意度的问题。在本文中，我们专注于满意的模量整数算术，该算法称为SMT（IA），包括线性和非线性整数算术理论。 SMT的主要方法依赖于以懒惰或渴望的好处来调用基于CDCL的SAT求解器。本地搜索是解决包括SAT在内的解决组合问题的一种竞争方法，但是SMT的研究尚未得到很好的研究。我们通过直接在变量上操作，突破传统框架来开发第一个用于SMT（IA）的本地搜索算法。我们通过考虑布尔和整数变量之间的区别来提出一个本地搜索框架。此外，我们设计了一个新颖的操作员和针对整数算术量身定制的评分功能，以及两级操作选择启发式功能。将这些组合在一起，我们开发了一个当地搜索SMT（IA）求解器，称为LS-IA。进行实验以评估Smtlib的基准上的LS-IA。结果表明，LS-IA具有竞争性，并且与最先进的SMT求解器互补，并且在仅具有整数变量的那些公式上表现良好。带有Z3的简单顺序组合可改善SMT-LIB可满足基准集的最新基准。
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.
