A Local Search Algorithm for MaxSMT(LIA)

本文关注的是带有线性整数算术背景理论的最大可满足模理论(MaxSMT(LIA))，它是可满足模理论(SMT)的一个重要推广，具有各种应用。我们设计了第一个局部搜索算法PairLS来解决MaxSMT(LIA)问题，其基于以下新思路：我们提出了一个新型运算符——成对运算符(pairwise operator)，它为整数变量提供了一种新的扩展局部搜索运算符的方式，同时操作两个变量，丰富了搜索空间。此外，我们还提出了一种补偿式选择启发式方法，以确定和区分成对运算符。我们进行了大量的实验来评估我们的算法，结果表明，我们的求解器与最先进的MaxSMT求解器具有竞争力。此外，我们还将成对运算符应用于增强SMT的局部搜索算法，证明了它的可扩展性。

设计一种新的局部搜索算法PairLS解决MaxSMT(LIA)问题，以及将pairwise操作应用于SMT的局部搜索算法中

设计pairwise操作来同时操作两个整数变量，拓展了原来的局部搜索算子，提高了搜索空间，使用基于补偿的选择启发式来确定pairwise操作，提高了算法效率

实验结果显示，PairLS算法在大规模基准测试中与现有的MaxSMT求解器相比具有竞争力，pairwise操作的应用也提高了SMT的局部搜索算法的效率，论文开源了实验代码和数据集

最近的相关研究包括：SMT和MaxSMT求解器的改进，以及局部搜索算法的优化，例如LocalSolver和Tabu Search等