A Local Search Algorithm for MaxSMT(LIA)
Xiang He, Bohan Li, Mengyu Zhao, Shaowei Cai
TL;DR
The paper addresses MaxSMT with Linear Integer Arithmetic (MaxSMT-LIA) by introducing PairLS, a novel local-search solver featuring a pairwise operator $p(v_1,v_2,val_1,val_2)$ that updates two integers simultaneously to escape local optima, and a compensation-based two-level picking heuristic to select such pairwise operations with respect to compensated literals. It integrates a $cm$ critical-move operator within the Integer mode of the existing LS-LIA framework and leverages a Weighting-PMS penalty scheme to steer the search across hard and soft clauses. Empirical results on large MaxSMT-LIA benchmarks show PairLS is competitive with state-of-the-art solvers OptiMathSAT and $ u Z$, with ablation studies confirming the effectiveness of the pairwise operator and the two-level picking heuristic; the approach also demonstrates extensibility by applying pairwise operations to SMT and exploring potential extensions to other theories. The work suggests that combining pairwise updates with compensation-based selection can significantly enhance local-search performance for SMT-related optimization problems and may inform future hybrid approaches that integrate local-search components with complete solvers.
Abstract
MaxSAT modulo theories (MaxSMT) is an important generalization of Satisfiability modulo theories (SMT) with various applications. In this paper, we focus on MaxSMT with the background theory of Linear Integer Arithmetic, denoted as MaxSMT(LIA). We design the first local search algorithm for MaxSMT(LIA) called PairLS, based on the following novel ideas. A novel operator called pairwise operator is proposed for integer variables. It extends the original local search operator by simultaneously operating on two variables, enriching the search space. Moreover, a compensation-based picking heuristic is proposed to determine and distinguish the pairwise operations. Experiments are conducted to evaluate our algorithm on massive benchmarks. The results show that our solver is competitive with state-of-the-art MaxSMT solvers. Furthermore, we also apply the pairwise operation to enhance the local search algorithm of SMT, which shows its extensibility.