A Local Search Algorithm for MaxSMT(LIA)
Xiang He, Bohan Li, Mengyu Zhao, Shaowei Cai

TL;DR
This paper introduces PairLS, a novel local search algorithm for MaxSMT with Linear Integer Arithmetic, featuring a pairwise operator and heuristic, demonstrating competitive performance on large benchmarks.
Contribution
The paper presents the first local search algorithm for MaxSMT(LIA) with a new pairwise operator and heuristic, extending local search capabilities for integer theories.
Findings
PairLS is competitive with state-of-the-art MaxSMT solvers.
The pairwise operator enhances local search for SMT.
The approach is extensible to other SMT algorithms.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFuzzy Logic and Control Systems · Constraint Satisfaction and Optimization · AI-based Problem Solving and Planning
