SLS-Enhanced Core-Boosted Linear Search for Anytime Maximum Satisfiability

A literal $\mathrm{\ell }$ is a $\{0,1\}$-valued variable $x$ or its negation $\overline{x}$. A clause $C\equiv {\sum }_i{\mathrm{\ell }}_i\ge 1$ is an at-least-one constraint and a (CNF) formula $F$ is a set of clauses. We will often treat clauses as the set of literals that appear in them. An objective $O$ is a pseudo-Boolean expression ${\sum }_i{c}_i{\mathrm{\ell }}_i$ where each $c_i$ is a positive integer. A (truth) assignment $\alpha$ maps variables to $0$ (which we identify with false) or $1$ (true). The semantics of assignments are extended to literals, clauses, and formulas in the standard way: $\alpha (\overline{x})=1-\alpha (x)$, $\alpha (C)=\max \{\alpha (\mathrm{\ell })\mid \mathrm{\ell }\in C\}$, and $\alpha (F)=\min \{\alpha (C)\mid C\in F\}$. The value (or cost) of $O$ under $\alpha$ is $\alpha (O)={\sum }_i{c}_i\alpha ({\mathrm{\ell }}_i)$. With a slight abuse of notation, we sometimes treat an objective $O$ as a set of its terms, i.e. write $c\mathrm{\ell }\in O$ if $O\equiv c\mathrm{\ell }+{\sum }_i{c}_i{\mathrm{\ell }}_i$. $\alpha$ is a solution of $F$ if $\alpha (F)=1$. $F$ is satisfiable if it has solutions and unsatisfiable if not.

We adopt two equivalent definitions of Weighted Partial Maximum Satisfiability (WPMS) to present core-boosted linear and stochastic local search (SLS). Specifically, SLS approaches are more naturally described in terms of the so-called clause-based definition of MaxSAT in which an instance $(F_H,F_S,w)$ consists of two formulas, the hard clauses $F_H$, the soft clauses $F_S$, and a weight function $w$ that associates a positive integer weight $w(C)$ to each soft clause $C\in F_S$. The goal is to compute a solution $\alpha$ of $F_H$ that minimizes the cost $\text{cost}(F_S,w,\alpha )={\sum }_{C\in F_S}w(C)(1-\alpha (C))$, defined as the weights of falsified soft clauses. Core-boosted linear search (and indeed any approach that makes use of a CDCL SAT-solver) for MaxSAT is more natural to describe in terms of the so-called objective-based definition of MaxSAT in which an instance $(F,O)$ consists of a formula $F$ and an objective $O$. The goal is to minimize $O$ subject to $F$, i.e. compute a solution $\alpha$ of $F$ that minimizes $\alpha (O)$ over all solutions of $F$. For both definitions of MaxSAT a minimum-cost solution of $F$ is called an optimal solution of $F$. The optimum cost of the instance is the cost of an optimal solution. In anytime MaxSAT solving, the goal is to compute a solution of as low cost as possible within some fixed amount of computational resources, typically computation time.

For intuition on the equivalence between the clause-based and the objective-based definitions of MaxSAT, note that a term $c\mathrm{\ell }$ of an objective can be viewed as a soft clause $(\overline{\mathrm{\ell }})$ with weight $c$. Thus, any objective-based instance $(F,O)$ can be seen as the clause-based instance $(F,\{(\overline{\mathrm{\ell }})\mid c\mathrm{\ell }\in O\},w)$ where $w((\overline{\mathrm{\ell }}))=c$ whenever $c\mathrm{\ell }\in O$. In the other direction, a clause-based instance $(F_H,F_S,w)$ can be viewed as an objective-based instance $(F_H\cup \{C\vee b_C\mid C\in F_S\},{\sum }_{C\in F_S}w(C)b_C)$ formed by: (i) extending each soft clause $C$ with a fresh variable $b_C$, (ii) forming a formula that contains the hard clauses and the extended soft clauses, and (iii) forming an objective to be the sum of the weights of soft clauses and their extension variables. For more details on the transformation and the equivalence between the definitions, we refer the reader to [6].

Core-boosted linear search makes extensive use of incremental SAT-solving under assumptions and unsatisfiable cores. An unsatisfiable core of an objective-based MaxSAT instance $(F,O)$ is a clause $C$ that: (i) only contains variables that appear in the objective, and (ii) is satisfied (i.e. assigned to 1) by any solution to $F$. Notice that satisfying a core requires assigning at least one objective variable to $1$, thus incurring cost in $O$. In this sense, cores provide information on the lower bound of the optimal cost of the instance.

To see the connection between our clause-based definition of a core and the more classical one in terms of unsatisfiable subsets of constraints, note that requirement (ii) that all solutions to $F$ satisfy $C$ is equivalent to the formula $F\wedge {\bigwedge }_{\mathrm{\ell }\in C}\overline{\mathrm{\ell }}$ being unsatisfiable. Thus, our definition of a core could be viewed as the negation of an unsatisfiable subset of $F$ obtained by assigning each literal in $C$ to $0$ and simplifying accordingly.

In practice, cores of MaxSAT instances are extracted using incremental SAT solving under assumptions [22, 7]. We abstract the use of an incremental SAT solver (i.e. a decision procedure for propositional logic) into the function $\text{Inc-SAT-solve}(F,𝒜)$ where $F$ is a CNF-formula and $𝒜$ is a set of literals, typically called assumptions. The call returns a triplet $(\text{sat?},C,\alpha )$. If sat? is true, then $\alpha$ is a solution to $F$ that extends $𝒜$, i.e. assigns $\alpha (\mathrm{\ell })=1$ for all $\mathrm{\ell }\in 𝒜$. Otherwise (if sat? is false), no such solution exists, and $C$ is a clause satisfied by any solution of $F$ containing negations of some of the literals in $𝒜$. Notice that $F$ has solutions iff $\text{Inc-SAT-solve}(F,\mathrm{\varnothing })$ returns true. Unsatisfiable cores of MaxSAT instances are then extracted by having $𝒜$ contain negations of objective variables. Practically all modern SAT solvers offer an assumption interface out of the box [22, 7].

Figure 1 overviews core-boosted linear search for computing a low-cost solution to a (clause-based) MaxSAT instance $(F_H,F_S,w)$ [10]. Core-boosted search consists of three separate phases: preprocessing, core-guided search, and solution-improving search. Each phase can – in theory – find and identify an optimal solution to the instance. More importantly, each phase will also modify and simplify the instance, and the following phase is always invoked on the modified instance rather than the original one. Intuitively, this allows core-boosted search never to be much worse than any individual phase, while also allowing subsequent phases to benefit from deductions made in previous ones. We next detail all three phases.

Algorithm 1 details the overall structure of a stochastic local search (SLS) algorithm for computing a low-cost solution to a clause-based MaxSAT instance $(F_H,F_S,w)$. In addition to the instance itself, the algorithm expects a user-specified parameter on how long to search for. In contrast to the algorithms that make use of a SAT solver, an SLS approach is, in general, not able to identify optimal solutions, which makes the limit parameter mandatory. A typical way of limiting the run time of SLS approaches is to enforce a maximum number of flips max-flips and terminate the search if no improving solutions have been found within max-flips flips. Finally, the algorithm also expects a solution $\alpha$ of $F_H$ as input. In the general setting, an SLS algorithm can be invoked using any assignment of the variables in $F_H\cup F_S$. However, prior work has shown that invoking an SLS approach with a solution of $F_H$ leads to much better performance in terms of the cost of the final solution being found. Since we are working on different ways of integrating SLS with SAT-based approaches to MaxSAT, we can assume that we always have access to some solution of the instance being solved. In our setting, such a solution can be obtained, e.g. by invoking the SAT solver on the hard clauses.

Algorithm 1 begins by initializing its best-known solution ${\alpha }_{\mathrm{𝑏𝑒𝑠𝑡}}$ to equal the input solution $\alpha$ and a flip counter to $0$ on Line 1. Afterward, the SLS weights $w^{\text{sls}}$ for all clauses in $F_H\cup F_S$ are initialized. Importantly, these are not the same as the weights of the soft clauses in the instance given by $w$. Instead, $w^{\text{sls}}$ will be used to define the score of each variable.

In other words, the score of a variable $x$ is the difference in the sum of weights wrt $w^{\text{sls}}$ of falsified clauses (hard or soft) when flipping the variable $x$. Informally speaking, flipping a variable $x$ with a high positive score will result in the current solution improving. With this intuition, the main loop (Lines 3 to 9) first checks on Line 4 whether the current assignment ${\alpha }^{\prime }$ is a solution of lower cost than the best know, and if it is, the best-known solution and best-cost are updated. Additionally, the flip counter (flip-count) is reset to $0$. Note specifically that the flip counter measures the number of flips since the last improvement to the solution was found. Afterward, the existence of so-called decreasing variables is checked. Here a variable is decreasing if its score is positive since flipping variables with a positive score decreases the cost of the assignment wrt $w^{\text{sls}}$ (cf. Definition 5). If no such variables exist, the algorithm has encountered a local optimum, and the SLS weights $w^{\text{sls}}$ are updated to escape it. Note that practical implementations of SLS algorithms directly modify and store the score of affected variables as well. Finally, a variable is selected, and the current assignment is updated by flipping its value on Line 8, and the flip counter is increased on Line 9. Commonly, variable selection employs the Best from Multiple Selection (BMS) heuristic [14], where a fixed number of variables is drawn randomly with replacement, and the variable with the highest score is selected from those.

Different SLS algorithms differ mainly in how the SLS weights are built and updated, and the specific choice of weighting scheme is known to impact the empirical performance of the approach significantly. In our work, we make use of the so-called NuWLS 2.0 weighting scheme for MaxSAT that was introduced in the NuWLS-c-2023 solver [17] that won all four anytime tracks of the MaxSAT evaluation 2023 and has since been integrated into other, well-performing MaxSAT solvers as well [5, 11, 27, 39]. When solving a MaxSAT instance $(F_H,F_S,w)$ NuWLS 2.0 initializes the weight of each hard clause to $1$ and the weight of each soft clause to $0$. Informally, this encourages Algorithm 1 to initially flip variables more likely to satisfy the hard clauses. The way the weights are updated on Line 6 depends on if the current assignment $\alpha$ is a solution of $F_H$. If not, the weights of all falsified hard clauses are increased by $1$. Otherwise, if $\alpha (F_H)=1$, the weights of all soft clauses are increased by their tuned weight.

In other words, the tuned weight of a soft clause $c$ is $w(c)$ divided by the average weight of all soft clauses. Dividing by the average effectively distributes the tuned weights around $1$: clauses $c$ with smaller-than-average (respectively larger-than-average) $w(c)$ have a tuned weight $\in (0,1)$ (respectively $>1$).

A very natural way of integrating SLS with a core-boosted linear search would be to first run the preprocessing phase on the clause-based input instance to obtain the objective-based instance $(F,O+l{b}_1)$, then invoke a SAT solver on $F$ to obtain an initial solution $\alpha$, and finally invoke Algorithm 1 on $(F,O)$ with $\alpha$ as the initial assignment and use the ${\alpha }_{\mathrm{𝑏𝑒𝑠𝑡}}$ returned as an initial assignment for the rest of the core-boosted linear search. This idea is well-studied in the context of anytime MaxSAT and corresponds to the de facto way in which most state-of-the-art anytime MaxSAT solvers integrate SLS with a CDCL-based algorithm [39, 28, 17].

While the effectiveness of applying an SLS algorithm before a CDCL-based algorithm is well understood in anytime MaxSAT (as witnessed e.g. by the results of the latest MaxSAT evaluations), much less is known about the relative effectiveness of running an SLS algorithm on a clause-based MaxSAT instance compared to the objective-based MaxSAT instances obtained after preprocessing. In this work, we study the effect of running Algorithm 1 both before and after the preprocessing phase of the core-boosted search. More precisely, given $(F,O+l{b}_1)$, we first call $\text{Inc-SAT-solve}(F,\mathrm{\varnothing })$ in order to obtain a solution $\alpha$ of $F$ which we use as a starting point to invoke Algorithm 1 on the instance $(F,O)$, and obtain a solution ${\alpha }^{\prime }$ (potentially equal to $\alpha$). Then, we invoke Algorithm 1 on the instance $(F_H,F_S,w)$ using the solution ${\alpha }^R$ of $F_H$ that corresponds to the solution ${\alpha }^{\prime }$ of $F$ as the initial assignment.

Notice that, especially when employing more advanced preprocessing rules like bounded variable elimination, the clauses in $F$ might significantly differ from those in $F_H\cup F_S$ and the relative effectiveness of Algorithm 1 in terms of the cost of the solution returned is an open question. Another important intuition here is that the solution $\beta$ returned by Algorithm 1 when invoked on $(F_H,F_S,w)$ need not be a solution of $F$, thus while the cost $\text{cost}(F_S,w,\beta )$ is an upper bound on the optimal cost of $(F,O+l{b}_1)$, $\beta$ can not be used for phase saving (cf. Section 2.3). In our implementation, we store $\beta$ throughout the rest of the core-boosted search, and in the end, compare the best solution found by core-boosted search with $\beta$ and return the better of the two.

During the core-guided phase of a core-boosted linear search, most of the SAT solver invocations are expected to return false and a new core. Core extraction essentially boils down to learning new clauses, and since SLS approaches can not learn new clauses nor determine that an instance is unsatisfiable, their applicability during the core-guided phase is limited. For general core-guided algorithms, SLS could conceivably help with heuristics that rely on finding intermediate solutions, most notably the so-called core exhaustion (also called cover optimization) technique [1, 36] that seeks to greedily strengthen the extracted cores with additional SAT calls under relaxed sets of assumptions. Since the PMRES [41] core-guided algorithm that the particular instantiation of core-boosted search we work with uses can not be extended with core exhaustion, we instead study ways in which the cores learned during this phase can be used to improve the performance of the SLS approach in the solution-improving phase where the goal is to compute new solutions, and SLS is expected to perform better. Additionally, we use the SLS approach at the end of the core-guided phase to find a low-cost solution to the instance obtained after the core-guided algorithm performs the core relaxation steps.

In contrast to the core-guided phase, the solution-improving phase of core-boosted linear search focuses on finding solutions of clauses in $F\cup \text{card}$ under different precisions (cf. Section 2.3) of $O^R$. An important intuition for integrating SLS with the phase is that the number of clauses required for encoding an objective improving constraint of the objective under a precision $\rho$ depends on the bound $B$. Thus, a low-cost (wrt $\lfloor O^R/\rho \rfloor$) solution can be used to decrease the number of clauses that need to be added to the SAT solver in the solution-improving phase and thus make the SAT calls faster to solve. To obtain such a solution, we invoke SLS on the instance $(F\cup \text{card},\lfloor O^R/\rho \rfloor )$ once for every precision considered during the phase. If the SLS algorithm finds a solution of cost $0$, the SAT solver is never invoked, instead the $\rho$ is lowered and the SLS algorithm invoked again.

Note, that these more frequent SLS calls can be performed without reinitializing the SLS solver. After the core-guided phase, we initialize the solver once with the instance $(F\cup \text{card},O^R)$. We directly modify the weights inside the SLS solver to apply the increasing precisions.

Our first experiment investigates different ways of invoking an SLS solver at the start of the search. For this, we consider two variants (described in more detail in Section 3.1) of the Base solver. The Init solver invokes SLS on the objective-based instance obtained after the initial conversion. This corresponds to the most common way in which modern SAT-based anytime solvers already use SLS in their search. The ExtInit solver extends the Init configuration by additionally invoking SLS on the original clause-based instance. Remember that, when preprocessing (which we denote by Preproc) is applied in the conversion from clause-based to objective-based, there can be a significant difference between the clause-based and the objective-based instance.

Figure 2 shows the results of the experiments. On unweighted instances, Preproc decreases the performance of Base, but Init improves the average score by $0.005$. ExtInit, however, is not as effective as Init only. On the weighted instances, ExtInit achieves a score $0.009$ higher than Init, and $0.031$ higher than Base. In contrast to the unweighted instances, Preproc improves the performance of Base and Init, yet still degrades that of ExtInit by $0.005$. We conclude that, on weighted instances, invoking an SLS search prior to the search of a SAT-based algorithm can perform noticeably better on the clause-based instance than on the objective-based one to the extent of being more effective than running preprocessing.

For unweighted instances, the linear search phase only has one precision level. Therefore, using SLS to extend a solution to the relaxed instance after the core-guided phase (AssignExt as described in Section 3.2) is practically equivalent to running SLS at the start of each precision level (IncPre as described in Section 3.3). Hence, we do not evaluate the latter on unweighted instances. Figure 3 shows the results of applying the two techniques in isolation, in combination with each other, and in combination with the best initial SLS routine for each of the two benchmark sets as determined in Section 4.1. AssignExt improves the score by $0.006$ for unweighted instances and profits from being paired with Init; the combination of the techniques yields an improvement of $0.011$. AssignExt, in isolation, also improves the score on the weighted instances (by $0.021$), and performs similarly to IncPre. However, when paired with ExtInit, IncPre outperforms every other possible combination, and yields an improvement of $0.036$ compared to Base.

In conclusion, both SLS integration techniques evaluated in this subsection improve the performance of Base, and yield the highest scores when paired with running SLS during the initial phase. In such a pairing, on weighted instances, however, IncPre outperforms AssignExt.

Figure 4 shows the effect of adding cores as clauses (CoreClauses) and using them to modify the SLS weighting scheme (CoreScores), as described in Section 3.2. For CoreScores, the core-factor parameter is set to $1$. Both AssignExt and IncPre benefit from CoreClauses, improving the score of AssignExt by $0.001$ on unweighted instances and by $0.008$ on weighted instances. The score of IncPre is improved by $0.003$. The CoreScores variant is not effective on unweighted instances, but on weighted instances its performance is comparable to CoreClauses when combined with IncPre, and slightly worse in conjunction with AssignExt.

The benefits of these (simplistic) approaches of using cores are overshadowed by invoking SLS at the beginning of the search; Init+AssignExt remains the best variant for unweighted instances and does not benefit from cores. On weighted instances, ExtInit+ IncPre wins, and adding a core strategy reduces the score. Yet, CoreClauses can help ExtInit+ AssignExt to achieve performance equivalent to ExtInit+ IncPre.

In conclusion, while SLS can benefit from the additional information generated in the core-guided phase, employing SLS before the search is more effective. Adding the cores as clauses yields higher scores than the weighting scheme modification introduced in this paper. Yet, both perform almost equivalently on weighted instances, making us carefully optimistic that more sophisticated weighting schemes based on cores could be developed.

Finally, we note that we did also compare our Base solver to the best-performing anytime solvers of the 2024 MSE (SPB_MaxSAT_Band and SPB_MaxSAT_FPS [28]) as well as Loandra as it participated in the 2024 MSE. Detailed results are presented in Appendix A, but the takeaway message is that the best-performing variant of our Base solver (Init+AssignExt for the unweighted instances and ExtInit+IncPre for the weighted) were still outperformed by the 2024 MSE version of Loandra by an average score of $0.018$ on unweighted and $0.010$ on weighted instances. To look into this, we ran the same experiments with a version of Base that uses Glucose as a backend. Without preprocessing, the conclusions with glucose as the backend were very similar to those presented in previous sections. When preprocessing with MaxPRE [29] was turned on, the performance of the solver improved significantly to the extent that any benefits from the SLS integration techniques disappeared. In short, we conclude that variants of Loandra that use Glucose as the backend benefit much more from preprocessing before search than from tighter SLS integration. In contrast, preprocessing has a significantly smaller impact when CaDiCaL is the backend, allowing us to observe benefits from SLS integration regardless. Currently, the best performance of Loandra is achieved with Glucose as the backend and preprocessing.

All in all, our results show that more sophisticated methods of integrating SLS with core-boosted linear search can result in increased performance, but the devil is in the details, and developing universally effective methods is a significant research challenge. We also note that the techniques we describe can be expected to work with any SLS approach for MaxSAT and that the approach implemented in BouMS is not state-of-the-art.