A Local Search Algorithm for MaxSMT(LIA)

The Satisfiability modulo theories (SMT) problem determines the satisfiability of a given quantifier-free first-order formula with respect to certain background theories. Here we consider the theory of Linear Integer Arithmetic (LIA), consisting of arithmetic formulae in the form of linear equalities or inequalities over integer variables ($\sum_{i=0}^{n}{a_{i}x_{i}\leq k}$ or $\sum_{i=0}^{n}{a_{i}x_{i}=k}$)¹¹1strict linear equalities in the form of ($\sum_{i=0}^{n}{a_{i}x_{i}<k}$) can be transformed to ($\sum_{i=0}^{n}{a_{i}x_{i}\leq k-1}$). An atomic formula can be a propositional variable or an arithmetic formula. A $literal$ is an atomic formula, or the negation of an atomic formula. A $clause$ is the disjunction of a set of literals, and a formula in conjunctive normal form (CNF) is the conjunction of a set of clauses. Given the sets of propositional variables and integer variables, denoted as $P$ and $X$ respectively, an assignment $\alpha$ is a mapping $X\rightarrow Z$ and $P\rightarrow\{false,true\}$, and $\alpha(x)$ denotes the value of a variable $x$ under $\alpha$.

The (weighted partial) MaxSAT Modulo Theories problem (MaxSMT for short) is generated from SMT. The clauses are divided into $hard$ clauses and $soft$ clauses with positive weight.

MaxSMT aims to find a feasible solution with minimal $cost$, that is, to find an assignment satisfying all hard clauses and minimizing the sum of the weights of the falsified soft clauses. The MaxSMT problem with the background theory of LIA is denoted as MaxSMT(LIA).

The clause weighting scheme is a popular local search method that associates an additional property (which is an integer number) called penalty weight to clauses and dynamically adjusts them to prevent the search from getting stuck in a local optimum. We adopt the weighting scheme called Weighting-PMS [19] to instruct the search. Weighting-PMS has been applied in state-of-the-art local search solvers for MaxSAT, such as SATLIKE [19] and SATLIKE3.0 [8]. When the algorithm falls into a local optimum, the Weighting-PMS dynamically adjusts the penalty weights of hard and soft clauses to guide the search direction.

Note that the penalty weight and the original weight of soft clauses are different. The goal of MaxSMT is to minimize the total original weight of unsatisfied soft clauses, while the penalty weight is updated during the search process, guiding the search in a promising direction.

Another key component of a local search algorithm is the operator, defining how to modify the current solution. When an operator is instantiated by specifying the variable to operate and the value to assign, an operation is obtained.

An operation is decreasing if its score is greater than 0. Note that given a set of clauses, denoted as $C$, the $score$ of operation $op$ on the subformula composed of $C$ is denoted as $score_{C}(op)$.

The original critical move operator only considers one single variable each time. However, it may miss potential decreasing operations. Specifically, when there exists no decreasing critical move operation, operations that simultaneously modify two variables may be decreasing, which are not considered by critical move.

Thus, the pairwise operator simultaneously modifying two variables is proposed to find a decreasing operation when there is no decreasing $cm$ operation.

The pairwise operator can be regarded as an extended neighborhood. When there exists no decreasing critical move operation, indicating that the local optimum of modifying individual variables is found, the search space can be expanded by simultaneously modifying two variables, and the solution may be further improved, thanks to the following property:

The proof can be found in Appendix 0.A. Recall the Example 3, the pairwise operation that simultaneously assigns $b$ to 2 and $c$ to 1, denoted as $op_{1}$, is decreasing, while none of the operations that individually assign $b$ to 2 and $c$ to 1, denoted as $op_{2}$ and $op_{3}$, is decreasing. The reason lies in that $b$ and $c$ both appear in the clause $c_{2}$, and $score_{\{c_{2}\}}(op_{1})>score_{\{c_{2}\}}(op_{2})+score_{\{c_{2}\}}(op_{3})$.

Motivation for compensation: Since one variable may exist in multiple literals, changing a variable will affect all literals containing the variable, and may make some originally true literals become false. Moreover, if the literal is the reason for some clauses being satisfied, i.e., it is the only true literal in the clause, then falsifying the literal also falsifies the clause.

Formally, for an operation $op$, we define a special set of literals $CL(op)=\{\ell|\ell$ is true and is the only true literal for some clauses, but $\ell$ would become false after individually performing $op\}$. After performing an operation $op$, the literals in the set $CL(op)$ are of special interest since some clauses containing such a literal would become falsified.

Concept of compensation: Let $op_{1}$ and $op_{2}$ denote two operations modifying individual variables. To minimize the disruptions that $op_{1}$ might wreak on the already satisfied clauses, another operation $op_{2}$ is simultaneously executed to make a literal $\ell\in CL(op_{1})$ remain true under the assignment after operating $op_{1}$. $op_{2}$ is denoted as compensation for $\ell$, and literals in the set $CL$ are denoted as Compensated Literals.

Compensation-based pairwise operation: A pairwise operation p($v_{1}$,$v_{2}$, $val_{1}$,$val_{2}$) can be regarded as simultaneously performing a pair of operations modifying individual variables, $op_{1}$ assigning $v_{1}$ to $val_{1}$ and $op_{2}$ assigning $v_{2}$ to $val_{2}$. The procedure to determine $op_{1}$ and $op_{2}$ is described as follows.

First, a candidate $op_{1}$ is chosen to satisfy a falsified clause. To this end, we pick a variable $v_{1}$ from a false literal $\ell_{1}$ in a random falsified clause, and $op_{1}$ is the corresponding cm operation, $cm(v_{1},\ell_{1})$. It prioritizes literals from hard clauses and soft clauses are considered only when all hard clauses are satisfied. To obtain sufficient candidates of $op_{1}$, $K$ (a parameter) literals are randomly selected from overall falsified clauses, and all variables in these literals are considered. The set of all candidate $op_{1}$ found in this stage is denoted as $CandOp$.

Second, given a literal $\ell_{2}\in CL(op_{1})$, the $op_{2}$ w.r.t $op_{1}\in CandOp$ is determined to guarantee that $\ell_{2}$ remains true after simultaneously performing $op_{1}$ and $op_{2}$, meaning that $op_{2}$ is selected to compensate for $\ell_{2}$. Specifically, to determine $op_{2}$, we pick a variable $v_{2}$ appearing in a literal $\ell_{2}\in CL(op_{1})$, and calculate the value $val_{2}$ according to $cm(v_{2},\ell_{2})$ assuming $op_{1}$ performed.

Note that there may exist multiple variables in the literal $\ell_{2}\in CL(op_{1})$, and thus given the operation $op_{1}$, and the literal $\ell_{2}$ selected in the second step, a set of pairwise operations is determined by considering all variables in $\ell_{2}$ except the variable in $op_{1}$, denoted as pair_set($\ell_{2}$,$op_{1}$).

Among the literals selected in the second step of determining a pairwise operation, we consider that some literals are more likely to become false, and should be given higher priority. Thus, we distinguish such literals from others. They are formally defined as follows.

A fragile literal with $\Delta=0$ is true as the inequality $\Delta\leq 0$ holds, but it can be falsified by any little disturbance that enlarges $\Delta$ of the corresponding fragile literal. Comparatively, a literal is safe means that even if the value of a variable in the literal changes comparatively larger (as long as $\Delta\leq 0$ after the modification), it remains true.

In the second step of determining a pairwise operation, among those compensated literals, we prefer fragile literals and prioritize the corresponding pairwise operations. Based on the intuition above, a two-level picking heuristic is defined:

• •

  We first choose the decreasing pairwise operation involving a fragile compensated literal.

• •

  If there exists no such decreasing pairwise operation, we further select the pairwise operation involving safe compensated literals.

Based on the picking heuristic, the algorithm for picking a pairwise operation is described in Algorithm 2. In the beginning, we initialize the set of pairwise operations involving fragile and safe compensated literals, denoted as $FragilePairs$ and $SafePairs$ (line 1). Firstly, $K$ (a parameter) false literals are picked from overall falsified clauses, and all critical move operations in these literals are added into $CandOp$ (lines 2–7). Note that it prioritizes hard clauses over soft clauses.

Then, for each operation $op_{1}\in CandOp$, we go through each compensated literal $\ell_{2}\in CL(op_{1})$. If $\ell_{2}$ is fragile (resp. safe), the set of corresponding pairwise operations determined by $pair\_set(\ell_{2},op_{1})$ are added to the $FragilePairs$ (resp. $SafePairs$) (line 8–13).

According to the two-level picking heuristic, if there exist decreasing operations in $FragilePairs$, we pick the one with the greatest $score$ (lines 14–15). Otherwise, we pick a decreasing operation in $SafePairs$ if it exists (lines 16–17). An operation with the greatest $score$ is selected via the BMS heuristic [7]. Specifically, the BMS heuristic samples $t$ pairwise operations (a parameter), and selects the decreasing one with the greatest $score$.

Implementation: PairLS is implemented in C++ and compiled by g++ with the ’-O3’ option enabled. There are 3 parameters in the solver: $L$ for switching modes; $t$ (the number of samples) for the BMS heuristic; $K$ denotes the size of $CandOp$. The parameters are tuned according to our preliminary experiments and suggestions from the previous literature. They are set as follows: $L=20$, $t=100$, $K=10$.

Competitors: We compare PairLS with 2 state-of-the-art MaxSMT solvers, namely OptiMathSAT(version 1.7.3) and $\nu Z$(version 4.11.2). OptiMathSAT applies MaxRes as the MaxSAT engine, denoted as Opt_res, while the default configuration encodes the MaxSMT problem as an optimization problem, denoted as Opt_omt. $\nu Z$ also has 2 configurations based on the MaxSAT engines MaxRes and WMax, denoted as $\nu Z$_res and $\nu Z$_wmax, respectively. The binary code of OptiMathSAT and $\nu Z$ is downloaded from their websites.

Benchmarks: Our experiments are conducted on 3 benchmarks. Those instances where the hard constraints are unsatisfiable are excluded, as they do not have feasible solutions.

Benchmark MaxSMT-LIA: This benchmark consists of 5520 instances generated based on SMT(LIA) instances from SMT-LIB³³3 https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_LIA. The original SMT(LI
A) benchmark consists of 690 instances from 3 families, namely bofill, convert, and wisa⁴⁴4SMT(LIA) instances from other families are excluded because most of them are in the form of a conjunction of unit clauses, and thus the generation method is not applicable, since each produced soft assertion is also a hard assertion.. We adopt the same method to generate instances as in previous literature [15]: adding randomly chosen arithmetic atoms in the original problem with a certain proportion as unit soft assertions. 4 proportions of soft clauses (denoted as $SR$) are applied, namely 10%, 25%, 50% and 100%. 2 MaxSMT instances can be generated from each original SMT instance, based on different ways to associate soft clauses with weights: one associates each soft clause with a unit weight of 1, and the other associates each soft clause with a random weight between 1 and the total number of atoms. Instances with unit weights and random weights are not distinguished as in [15]. The total number of instances is $690\times 2\times 4=5520$, where 690 denotes the number of original SMT(LIA) instances, 2 denotes 2 kinds of weights associated with soft clauses, and 4 denotes the 4 proportions of soft clauses. Note that the “bofill” family was adopted in [15], while the family of “convert” and “wisa” are new instances.

Benchmark MaxSMT-IDL: This benchmark contains 12888 new MaxSM-
T instances generated by the above method, based on 1611 SMT(IDL) instances including all families from SMT-LIB⁵⁵5 https://clc-gitlab.cs.uiowa.edu:2443/SMT-LIB-benchmarks/QF_IDL (similar to MaxSMT-LIA benchmark, the total number of instances is $1611\times 2\times 4=12888$). Instances with unit weights and random weights are also not distinguished when reporting results.

Benchmark LL: The benchmark was proposed in [14]. Unsatisfiable instances and instances over linear real arithmetic are excluded, resulting in 114 instances in total. 56 instances contain soft clauses with unit weights of 1, and 58 instances contain soft clauses with random weights ranging from 1 to 100. Instances with Unit weights and Random weights are distinguished as in [14].

Experiment Setup: All experiments are conducted on a server with Intel Xeon Platinum 8153 2.00GHz and 2048G RAM under the system CentOS 7.7.1908. Each solver executes one run for each instance in these benchmarks, as they contain sufficient instances. The cutoff time is set to 300 seconds for the MaxSMT-LIA and MaxSMT-IDL benchmarks as previous work [15], and 1200 seconds for the LL benchmark as previous work [14].

For each family of instances, we report the number of instances where the corresponding solver can find the best solution with the smallest $cost$ among all solvers, denoted by $\#win$, and the average running time to yield those best solutions, denoted as $time$. Note that when multiple solvers find the best solution with the same $cost$ within the cutoff time, they are all considered to be winners. The solvers with the most $\#win$ in the table are emphasized with bold value.

The solution found by solvers and the corresponding time are defined as follows: As for complete solvers, $\nu Z$ and OptiMathSAT, we take the best upper bound found within the cutoff time as their solution, and the time to find such upper bound is recorded by referring to the log file. Note that the proving time for complete solvers is excluded. As for PairLS, the best solution found so far within the cutoff time and the time to find such a solution are recorded.

Results on benchmark MaxSMT-LIA: As presented in Table 1, PairLS shows competitive and complementary performance on this benchmark. Regardless of the proportion of soft clauses $SR$, PairLS always leads in the total number of winning instances. On the “bofill” family, PairLS performs better on instances with larger $SR$, confirming that PairLS is good at solving hard instances. On the “convert” family, PairLS outperforms all competitors regardless of $SR$. On the “wisa” family, PairLS cannot rival its competitors. In Fig.3 of Appendix C, we also present the run time comparison between PairLS and the best configuration of competitors, namely $\nu Z$_res and Opt_res. The run time comparison indicates that PairLS is more efficient than Opt_res and is complementary to $\nu Z$_res.

Results on benchmark MaxSMT-IDL: As presented in Table 2, PairLS can significantly outperform all competitors regardless of the proportion of soft clauses. In the overall benchmark, PairLS can find a better solution than all competitors on 53.5% of total instances, and it can lead the best competitor by 1224 “winning” instances, confirming its dominating performance. In Fig.4 of Appendix C, we also present the run time comparison between PairLS and the best configuration of competitors, namely $\nu Z$_res and Opt_omt, indicating that PairLS is more efficient than competitors in instances with small $SR$.

Results on LL benchmark: The results are shown in Table 3. PairLS shows comparable but overall poor performance compared to its competitors on this benchmark. One possible reason is that the front-end encoding for these benchmarks would generate many auxiliary Boolean variables, while PairLS cannot effectively explore the Boolean structure as LS-LIA [9]. Specifically, the average number of auxiliary variables in this benchmark is 1220, while the counterparts in MaxSMT-LIA and MaxSMT-IDL are 327 and 528.

To be more informative in understanding how the solvers compare in practice, the evolution of the solution quality over time is presented. Specifically, we evaluate the overall performance on the MaxSMT-LIA and MaxSMT-IDL benchmark with 4 cutoff times, denoted as cutoff: 50, 100, 200, 300 seconds. Given an instance, the proportion of the $cost$ to the sum of soft clause weights is denoted as $cost_{P}$ ⁶⁶6If no feasible solution is found, then $cost_{P}$ is set as 1. Note that we present the average $cost_{P}$ rather than the average $cost$, since the $cost$ of certain instances can be quite large, dominating the average $cost$.. The average $cost_{P}$ over time is presented in Fig.LABEL:ev, showing that PairLS can efficiently find high-quality solutions within a short time. Moreover, we also report the “winning” instances over time. As shown in Table 7 in Appendix D, on each benchmark, PairLS leads the best competitor by at least 645 “winning” instances regardless of the cutoff time, confirming its dominating performance.

To analyze the effectiveness of our proposed strategies, two modified versions of PairLS are proposed as follows.

• •

  To analyze the effectiveness of pairwise operation, we modify PairLS by only using the critical move operator, leading to the version $v_{no\_pair}$.

• •

  To analyze the effectiveness of two-level heuristic in compensation-based picking heuristic for picking a pairwise operation, PairLS is modified by selecting pairwise operation without distinguishing the fragile and safe compensated literals, leading to the version $v_{one\_level}$.

We compare PairLS with these modified versions on 3 benchmarks. The results of this ablation experiment are presented in Table 4, confirming the effectiveness of the proposed strategies.

Moreover, we also analyze the extension for simultaneously operating on more variables. PairLS is modified by simultaneously modifying three variables, where the third variable is modified to compensate for the second one, leading to the version $v_{tuple}$. We conduct our experiments on MaxSMT-LIA. The results are in Apendix E. When $N=3$, the number of possible operations increases from O($k^{2}$) to O($k^{3}$), where $k$ is the number of variables in unsatisfied clauses. This might significantly slow down the searching process, indicating that modifying 2 variables simultaneously is the best choice of trade-off between cost and effectiveness.