Rethinking the Soft Conflict Pseudo Boolean Constraint on MaxSAT Local Search Solvers

1 Introduction

The Maximum Satisfiability problem (MaxSAT) is an optimization version of the famous Satisfiability problem (SAT). Given a propositional formula in Conjunctive Normal Form (CNF), MaxSAT aims to find an assignment that satisfies as many clauses as possible. More generally, the Partial MaxSAT (PMS) divides the clauses into hard and soft, aiming to satisfy as many soft clauses as possible while satisfying all the hard clauses. The Weighted PMS (WPMS) associates each soft clause with a positive weight, aiming to maximize the total weight of satisfied soft clauses while satisfying all the hard clauses. The nature of hard and soft clauses well matches the constraints and optimization objectives in optimization scenarios. Therefore, MaxSAT has a wide range of industrial and academic applications, such as group testing [Ciampiconi et al., 2020], timetabling [Lemos et al., 2020], planning [Bonet et al., 2019], clique problems [Jiang et al., 2018], set covering [Lei and Cai, 2020], etc.

∗Corresponding author.

Algorithms for MaxSAT can be divided into complete and incomplete solvers based on their capacity to provide optimality guarantees. Complete algorithms include branch and bound [Cherif et al., 2020; Li et al., 2021] algorithms and a series of methods that solve MaxSAT by iteratively calling a SAT solver, so-called SAT-based algorithms [Fu and Malik, 2006; Ans´otegui et al., 2013; Nadel, 2019]. Due to the power of complete solving techniques in handling CNF formulas, such as the unit propagation [Davis et al., 1962; Li et al., 2005] and clause learning [Silva and Sakallah, 1996; Li et al., 2020], complete algorithms exhibit excellent performance for solving MaxSAT.

Another important technique inMaxSAT complete-solving is the Soft conflict Pseudo Boolean (SPB) constraints [Berg et al., 2019; Li et al., 2021]. A Pseudo Boolean (PB) constraint [Chu et al., 2023c; Zhou et al., 2023] is a particular type of linear constraint in the form of ∑ni=1 qixi # K, where # ∈ {<,≤,=,≥,>} and can be normalized to <, qi and K are integer constants, and xi are 0/1 variables, i ∈ {1, ..., n}. In many complete MaxSAT solvers, once a better solution is found, a PB (or Cardinality for unweighted problem) constraint [Roussel and Manquinho, 2021] is added naturally to prohibit the procedure from finding solutions that are no better than the current best. Falsifying such a constraint leads to a Soft conflict [Li et al., 2021]. The SPB constraints can help complete solvers prune branches and reduce the search space.

On the other hand, incomplete algorithms mainly focus on the local search approach [Selman et al., 1993; Morris, 1993; Cha et al., 1997]. With the development of many local search techniques, including the decimation-based initialization methods [Cai et al., 2017], the local optima escaping methods [Zheng et al., 2022b; Zheng et al., 2023], and especially the clause weighting methods [Lei and Cai, 2018; Cai and Lei, 2020; Chu et al., 2023b], the state-of-the-art local search algorithms exhibit competitive performance with complete algorithms and even dominating the rankings of incomplete tracks of recent MaxSAT Evaluations.

In this paper, we focus on the local search approach for MaxSAT and propose two new methods regarding the clause weighting scheme, i.e., integrating SPB constraints into the clause weighting system and a novel Adaptive Clause Weighting scheme.

We first introduce the SPB constraints into the local search MaxSAT algorithm. Similar constraints have also been applied to local search for Pure MaxSAT [Cai and Zhang, 2020], a special case of MaxSAT whose hard clauses have only positive literals and soft clauses are all unit clauses with negative literals (and vice versa), and it is used as a hard constraint to strictly restrict the search space, which may limit the search ability of the local search.

To better and more generally make use of the SPB constraints, we propose to integrate them into the clause weighting system for universal MaxSAT problems, including PMS and WPMS. Specifically, we associate each hard clause with a dynamic weight and add a SPB constraint to the MaxSAT formula with a dynamic weight. Once the algorithm falls into a local optimum, the dynamic weights of the hard clauses and the SPB constraint falsified by the current local optimal solution will be increased. Moreover, once a better solution is found by local search, the SPB constraint will be updated accordingly. In this way, the SPB constraint does not restrict the search space but guides the search directions and leads the algorithm to find better solutions.

For the second method, we found that the existing clause weighting methods usually update the dynamic weight of each clause using a constant value, which may make the increased rate of dynamic weights converge inversely proportional to the number of weight increments and approaches zero. The convergence of the increased rate may lead to the distribution of dynamic weights tending to stabilize, diminish the effect of the clause weighting method, and make it hard for the algorithm to escape from local optima. There are some techniques for avoiding the convergence of the increased rate caused by the divergent increased dynamic weights, including setting upper limits, periodic decay, and probabilistic smoothing [Cai et al., 2015; Lei and Cai, 2018]. However, setting upper limits may restrict the search flexibility, the decay method cannot handle the convergence during each decay, and the weight smoothing method should set lower limits, which may also restrict the search flexibility.

To handle these issues, we propose a simple clause weighting method that allows the dynamic weights to update adaptively. Specifically, we increase the dynamic weights proportionally according to the current weights. Such a strategy provides a lower bound for the increased rate of dynamic weights and makes the clause weighting method always guide the search directions and help escape from local optima efficiently. As a result, our method is simple yet effective, providing a new perspective on the clause weighting methods.

In the end, by integrating the above two methods, we propose a new local search MaxSAT algorithm called SPBMaxSAT. SPB-MaxSAT always maintains an SPB constraint and associates it with a dynamic weight, which will be increased proportionally once a local optimal solution falsifies the constraint. We further combine SPB-MaxSAT with a typical SAT-based solver, TT-Open-WBO-Inc [Nadel, 2019], as many incomplete MaxSAT solvers do [Lei et al., 2021; Chu et al., 2022], and the resulting incomplete solver is denoted as SPB-MaxSAT-c. Extensive experiments show that SPBMaxSAT significantly outperforms the state-of-the-art local search MaxSAT algorithms, NuWLS [Chu et al., 2023b] and BandMaxSAT [Zheng et al., 2022b]; SPB-MaxSAT-c also exhibits higher performance and robustness than NuWLS-c-

2023 [Chu et al., 2023a], winner of all the four incomplete tracks of MaxSAT Evaluation 2023.

2 RelatedWork

This section first reviews the development of the clause weighting method in local search MaxSAT algorithms and then introduces related works that use complete solving techniques of SAT and MaxSAT for the local search. We will also briefly describe the differences and improvements of our method over the existing studies.

2.1 ClauseWeighting inMaxSAT Local Search

Clause weighting is a typical technique in local search SAT and MaxSAT solvers [Frank, 1996; Cha et al., 1997]. It associates the clauses with dynamic weights and uses them to guide the search directions. The main idea is that when the algorithm falls into a local optimum, i.e., flipping any variable cannot improve the current solution, the dynamic weights of falsified clauses will be increased to help the algorithm escape from local optima. With the appearance of PMS and WPMS, many advanced clause weighting methods have been proposed to consider the properties of hard and soft clauses. For instance, Dist [Cai et al., 2014] and CCEHC [Luo et al., 2017] only use clause weighting methods upon hard clauses and prioritize satisfying hard clauses during the search. SATLike [Lei and Cai, 2018] and its extension of SATLike3.0 [Cai and Lei, 2020] first propose to associate both hard and soft clauses with dynamic weights, which is also inherited by BandMaxSAT [Zheng et al., 2022b] and FPS [Zheng et al., 2023] algorithms. Recently, NuWLS [Chu et al., 2023b] improves the clause weighting method by assigning appropriate initial dynamic weights to the clauses, and NuWLS-c-2023 [Chu et al., 2023a] further proposes to uniformly update the dynamic weights of all soft clauses, helping it win all the four incomplete tracks of MaxSAT Evaluation 2023.

The clause weighting method has made significant achievements in the field of MaxSAT solving. In this work, we investigate the limitation of constant increments of existing clause weighting methods used in the above algorithms and thereby propose an effective adaptive clause weighting strategy to address the limitation.

2.2 Complete SolvingMethods in Local Search

Since complete algorithms occupy the mainstream of (Max)SAT solvers, researchers usually use local search to improve complete solvers [Cai and Zhang, 2021; Chu et al., 2023a] but rarely try to use complete solving methods to improve local search incomplete solvers. There are some studies that use unit propagation [Davis et al., 1962; Li et al., 2005] techniques to generate the initial assignments for local search (Max)SAT algorithms, obtaining significant improvements. The linear search constraint has been used in the local search process by strictly restricting the search space for a special case of MaxSAT [Cai and Zhang, 2020], showing excellent performance in the special MaxSAT problems that are very easy to find feasible solutions. However, strictly restricting the search space might not be appropriate for general MaxSAT problems.

This paper also investigates the utilization of complete solving methods, i.e., SPB constraint, in MaxSAT local search solvers and proposes to integrate SPB into the clause weighting system rather than directly restrict the search space. The clause weighting scheme with the SPB constraint can guide the algorithm to find better solutions, as demonstrated by our follow-up experiments on various MaxSAT problems.

3 Preliminaries

Given a set of Boolean variables {x1, · · · , xn}, a literal is either a variable itself xi or its negation ¬xi, a clause is a disjunction of literals, e.g., c = l1∨· · ·∨lp, and a Conjunctive Normal Form (CNF) formula F is a conjunction of clauses, e.g., F = c1 ∧ · · · ∧ cq. A complete assignment A represents a mapping that maps each variable to a value of 1 (true) or 0 (false). A literal xi (resp. ¬xi) is satisfied if the current assignment maps xi to 1 (resp. 0). A clause is satisfied by the current assignment if there is at least one satisfied literal in the clause and is falsified otherwise.

Given a CNF formula F, the MaxSAT problem aims to find an assignment (i.e., solution) that satisfies as many clauses in F as possible. Given a CNF formula F whose clauses are divided into hard and soft, we denote Hard(F) and Soft(F) as the set of hard and soft clauses in F, respectively. The Partial MaxSAT (PMS) problem is a variant of MaxSAT that aims to find an assignment satisfying all the hard clauses while maximizing the number of satisfied soft clauses in F. The Weighted Partial MaxSAT (WPMS) problem is a generalization of PMS where each soft clause is associated with a positive weight, aiming to find an assignment that satisfies all the hard clauses while maximizing the total weight of satisfied soft clauses in F.

For convenience, we regard PMS as a special case of WPMS by assigning each soft clause with unit weight. Given a MaxSAT instance F , we denote ws(c) as the original weight of soft clause c ∈ Soft(F) and denote wh(c) as the dynamic weight maintained of each hard clause c ∈ Hard(F) by the clause weighting method.

Given a MaxSAT instance F, a complete assignment A is feasible if it satisfies all the hard clauses in F, and we denote its objective function obj(A) as the total weight of soft clauses falsified by A and set its cost function cost(A) to obj(A) (resp. +∞) if A is feasible (resp. infeasible). Moreover, in the local search algorithms for MaxSAT, the widely-used flipping operator for a variable is an operator that changes its Boolean value.

4 The Proposed SPB-MaxSAT

This section introduces our proposed local search algorithm, termed the Soft conflict Pseudo Boolean based MaxSAT solver (SPB-MaxSAT). SPB-MaxSAT maintains an SPB constraint with dynamic weight during the local search process, integrating SPB into the clause weighting system and using an adaptive clause weighting technique to update its dynamic weight. The clause weighting system is then used to help the algorithm escape from local optima and find better solutions.

Algorithm 1: SPB-MaxSAT

Input: MaxSAT instance F, cut-off time cutoff, BMS parameter k, hard clause dynamic weight increment hinc, increase proportion δ Output: A feasible solution A of F, or no feasible solution found 1 A←an initial complete assignment; 2 A∗ ←A; 3 for each c ∈ Hard(F) do 4 wh(c) ← 1; 5 w(SPB) ← 1; 6 while running time < cutoff do 7 if D ← {x|score(x) > 0} ̸= ∅ then 8 v ← a variable in D picked by BMS(k); 9 else 10 Update dynamic weights by SPB-Weighting; 11 if ∃ falsified hard clauses then 12 c ← a random falsified hard clause; 13 else 14 c ← a random falsified soft clause; 15 v ← the variable with the highest score in c; 16 A←Awith v flipped; 17 if cost(A) < cost(A∗ ) then 18 A∗ ← A; 19 update SPB accordingly; 20 if A∗ is feasible then return A∗ ; 21 else return no feasible assignment found;

In the following, we first present the main framework of SPB-MaxSAT and then introduce the clause weighting system in SPB-MaxSAT with the SPB constraint and the adaptive clause weighting method.

4.1 The Main Framework

SPB-MaxSAT actually follows the general framework of many local search algorithms, such as SATLike3.0 [Cai and Lei, 2020] and NuWLS [Chu et al., 2023b], and uses our proposed clause weighting scheme. The main procedure of SPB-MaxSAT is shown in Algorithm 1. The algorithm first generates an initial complete assignment A by the decimation method [Cai et al., 2017] used in SATLike3.0 and NuWLS, initializes the best solution found A∗ , and initializes the dynamic weights (lines 1-5). Then, the algorithm repeats selecting a variable and flipping it until the cut-off time is reached (lines 6-19). If there are variables with positive score, the algorithm also uses the Best-from-Multiple-Selections (BMS) strategy [Cai, 2015] used in various local search MaxSAT algorithms to select a variable with positive score (lines 7-8). BMS chooses k random variables with positive score (with replacement) and returns the one with the highest score.

Upon falling into a local optimum, SPB-MaxSAT first updates the dynamic weights by our proposed clause weighting system with the SPB constraint (line 10), which is encapsulated by the SPB-Weighting function introduced in Section 4.2. Then, if the current local optimal solution is infeasible

(resp. feasible), a random falsified hard (resp. soft) clause c is selected, and the variable to be flipped is the one with the highest score in c (lines 11-15). Once a better feasible solution is found, A∗ will be updated, and the SPB constraint will also be updated accordingly.

4.2 ClauseWeighting System

This subsection presents our proposed SPB constraint, scoring function, and adaptive SPB weighting method together with our intuition.

SPB Constraint

Suppose A∗ is the best solution found so far during the local search. Then, finding solutions no better than A∗ is meaningless, and an SPB constraint, denoted as SPB, is added naturally as follows.

where unsat(c) equals 1 (resp. 0) if clause c is falsified (resp. satisfied) by the current solution A and can be regarded as a Boolean variable. Actually, SPB can be simply represented by obj(A) < cost(A∗ ), and it will be updated accordingly with the updating of A∗ .

In SPB-MaxSAT, we associate SPB with a dynamic weight w(SPB), using w(SPB) and the dynamic weights of hard clauses to calculate the scoring function of the variables and guide the search directions.

Scoring Function

In the local search MaxSAT algorithms, the scoring function score(v) of a variable v is widely used to evaluate the benefit of flipping v in the current solution. In our SPB-MaxSAT, score(v) is calculated by combining the influences of such a flipping on the hard clauses and the SPB constraint.

Given a MaxSAT instance F, the current solution A, the dynamic weight wh(c) of each hard clause c, and the dynamic weight w(SPB) of SPB, we denote hscore(v) as the decrement of the total dynamic weight of falsified hard clauses caused by flipping v in A. Suppose A′ is the solution obtained by flipping variable v in A. We define another scoring function, SPBscore(v), to evaluate the influence of flipping v in A to the SPB constraint as follows.

Finally, the scoring function score(v) is defined as follows:

The dynamic weights wh(c) and w(SPB) actually play the role of a pivot to control the importance of the hard clauses and soft clauses in the MaxSAT solving process. The SPBscore(v) actually regards all soft clauses as a whole and evaluates the influence on the objective function obj(A) caused by flipping v. In our method, the clause weighting technique is used to adjust wh(c) and w(SPB), so as to adjust the precedence of satisfying hard clauses and increasing the objective function. As a result, the adaptively adjusted SPB Constraint and w(SPB) dynamic weight can lead the local search algorithm to better solutions.

Algorithm 2: SPB-Weighting

Input: MaxSAT instance F, current solution A, hard clause dynamic weight increment hinc, increment proportion δ

• 1 for each clause c ∈ Hard(F) falsified by A do
• 2 wh(c) ←wh(c) +hinc;
• 3 if SPB is falsified by A then
• 4 w(SPB) ← δ · (w(SPB) +1);

Adaptive SPB Weighting

The initial values of the dynamic weight wh(c) of each hard clause c and the dynamic weight w(SPB) of SPB are both set to 1. We propose an SPB-Weighting function shown in Algorithm 2 to update the dynamic weights once the algorithm falls into a local optimum, i.e., there is no variable having a positive score.

The SPB-Weighting function is very simple and easy to understand. This function just increases the dynamic weights of falsified elements in the current local optimal solution, including hard clauses and the SPB constraint. The dynamic weights of falsified hard clauses are increased by a constant parameter hinc as many local search MaxSAT algorithms do [Lei and Cai, 2018; Zheng et al., 2022b; Chu et al., 2023b], and the dynamic weight of SPB is updated adaptively by first increasing 1 and then multiplying by δ > 1. Actually, the original constant clause weighting method can be regarded as a special case of our adaptive clause weighting method with δ = 1. Moreover, to avoid w(SPB) from becoming too large, we also use a decay method to reduce all the dynamic weights simultaneously when they reach a threshold.

Discussion on Adaptive Clause Weighting

The adaptive clause weighting method in function SPBWeighting actually highlights the soft clauses and better solutions in the later stages of the search. At the beginning of the search, when there is no feasible solution found, cost(A∗ ) = +∞ holds, SPB is always satisfied, and w(SPB) always equals 1. The algorithm mainly pays attention to finding feasible solutions. After finding a feasible solution, w(SPB) will be increased once SPB is falsified to pay more attention to soft clauses and push the algorithm to find better solutions. However, with the accumulation of the dynamic weights, increasing w(SPB) by 1 might only have a minor influence on the importance of soft clauses, and the algorithmmight need more steps to pay appropriate attention to the soft clauses.

Suppose the average dynamic weights of hard clauses, denoted as wh(c), increases by 1 once w(SPB) increases. For each increment of w(SPB), i.e., w′ (SPB) = δ·(w(SPB)+ 1), we define the increasing rate as Rinc = (w′ (SPB) - w(SPB))/w(SPB) and the increment on the importance of soft clauses as Iinc = (w′ (SPB) -w(SPB))/(w(SPB) + wh(c)). The smaller the Rinc and Iinc, the smaller the effect of the increment of w(SPB) for guiding the search. Figure 1 shows how these two metrics change with the increment of the number of times w(SPB) increased when δ = 1.001 (i.e., adaptive weighting) and 1 (i.e., constant weighting). We can observe that both the two metrics converge to δ - 1, i.e., zero when δ = 1. Therefore, increasing w(SPB) proportionally with δ > 1 can avoid the diminishing of the clause weighting method for guiding the search with the accumulation of the dynamic weights.

In addition, for the hard clauses, we increase their dynamic weights conservatively to ensure that we can find high-quality feasible solutions. The experimental results also show that increasing w(SPB) proportionally is better than increasing both wh(c) and w(SPB) proportionally or linearly with a constant value, demonstrating that our design is reasonable and effective.

5 Experiments

In this section, we first compare the proposed SPB-MaxSAT 1 algorithm with the state-of-the-art local search algorithms, NuWLS [Chu et al., 2023b] and BandMaxSAT [Zheng et al., 2022b]. We then combine SPB-MaxSAT with a SAT-based solver, TT-Open-WBO-Inc [Nadel, 2019], as many incomplete MaxSAT solvers do [Lei et al., 2021; Chu et al., 2022], and compare the resulting incomplete solver SPB-MaxSATc with the state-of-the-art incomplete solver NuWLS-c-2023, which won all the four incomplete tracks of MaxSAT Evaluation (MSE) 2023. NuWLS-c-2023 is an improvement of NuWLS-c [Chu et al., 2022], the winner of all the four incomplete tracks of MSE2022. Since they obtained such good results on recent MSEs, we only selected NuWLS-c-2023 as the baseline of incomplete solver and ignored other effective solvers, such as DT-HyWalk [Zheng et al., 2022a], Loandra [Berg et al., 2019], and TT-Open-WBO-Inc [Nadel, 2019]. Finally, we perform ablation studies to analyze the effectiveness of our adaptive clause weighting method by comparing SPB-MaxSAT with its variant algorithms.

5.1 Experimental Setup

All the algorithms were implemented in C++ and run on a server using an AMD EPYC 7H12 CPU, running Ubuntu 18.04 Linux operation system. We evaluated the algorithms on all the PMS and WPMS instances from the incomplete track of the six recent MSEs 2 , i.e., MSE2018 to MSE2023. Note that the benchmarks containing all PMS/WPMS instances from the incomplete track of MSE2023 are named PMS 2023/WPMS 2023, and so forth. Each instance was processed once by each algorithm with two time limits, 60 and 300 seconds. This is consistent with the settings of the incomplete track of MSEs.

1 https://github.com/JHL-HUST/SPB-MaxSAT

We adopt two kinds of metrics to compare and evaluate the algorithms. The first one is the number of winning instances, represented by '#win', which indicates the number of instances in which the algorithm yields the best solution among all the algorithms listed in the table. The metric '#win' has been widely used in comparing local search MaxSAT algorithms [Cai et al., 2014; Luo et al., 2017; Lei and Cai, 2018; Cai and Lei, 2020; Chu et al., 2023b; Zheng et al., 2022b].

The second one is the scoring function used in the incomplete track of MSEs. The score of a solver for an instance is 0 if the solver cannot find feasible solutions, and (BKC + 1)/(cost(A) + 1) otherwise, where A is its output feasible solution, and BKC is the best-known cost of the instance. The score of a solver for a benchmark is its average score upon all contained instances, represented by '#score'. The best results appear in bold in the tables.

Parameters in SPB-MaxSAT mainly include the BMS parameter k, the hard clause dynamic weight increment hinc, and the increase proportion δ. Note that parameters k and hinc are also used in the baseline algorithms, and our method only introduces one additional parameter. We adopt an automatic configurator called SMAC3 [Lindauer et al., 2022] to tune the parameters based on instances in the incomplete track of MSE2017. Note that SMAC3 is also widely used for tuning the baseline solvers, NuWLS and NuWLSc-2023. The tuning domains of the above parameters are k ∈ [50, 100], hinc ∈ [1, 30], and δ ∈ [1.0005, 1.002]. The final settings of these parameters in both SPB-MaxSAT and SPB-MaxSAT-c are k = 53, hinc = 1, and δ = 1.00072 for PMS and k = 97, hinc = 28, and δ = 1.001 for WPMS. Parameters in variant algorithms of SPB-MaxSAT in the ablation study are also tuned by SMAC3.

5.2 Comparison with Local Search Baselines

The comparisons of SPB-MaxSAT with NuWLS and BandMaxSAT are summarized in Tables 1 and 2, respectively. From the results, one can see that SPB-MaxSAT exhibits significantly better performance than the two local search baselines in both PMS and WPMS instances, irrespective of the 60s or 300s time limit, according to the '#win' and '#score' metrics. Specifically, the number of '#win' instances of SPBMaxSAT is 47-118% (resp. 68-217%) more than NuWLS (resp. BandMaxSAT) for PMS benchmarks and 353-641% (resp. 84-263%) more than NuWLS (resp. BandMaxSAT) for WPMS benchmarks. The '#score' of SPB-MaxSAT is 17% (resp. 9-18%) higher than NuWLS (resp. BandMaxSAT) for PMS benchmarks and 4-17% (resp. 9-24%) higher than NuWLS (resp. BandMaxSAT) for WPMS benchmarks.

2 https://maxsat-evaluations.github.io/

The improvement of SPB-MaxSAT over the baselines in WPMS instances is more obvious because there are many PMS instances in the MSE benchmarks that are simple and can be solved to optimal for these effective local search algorithms. Moreover, SPB-MaxSAT and NuWLS actually differ only in their clause weighting system and have the common variable selection strategy and searching framework, and BandMaxSAT has a different searching framework that applies the multi-armed bandit model to help select the search directions. The results show that BandMaxSAT has a better complementarity with SPB-MaxSAT (i.e., more '#win' instances) than NuWLS in WPMS benchmarks, indicating that our proposed clause weighting system has a relatively comprehensive improvement compared to that in NuWLS.

In summary, our proposed methods that combine our SPB constraint with clause weighting system and adaptive clause weighting strategy help SPB-MaxSAT significantly outperform the state-of-the-art local search MaxSAT algorithms.

5.3 Combining with SAT-based Solver

The comparison results between SPB-MaxSAT-c and NuWLS-c-2023 are shown in Table 3. They all combine their local search components, i.e., SPB-MaxSAT and an improvement of NuWLS, with a SAT-based solver, TT-Open-WBOInc. They first use a SAT solver to generate a feasible assignment as an initial solution, then call the local search algorithm to continue the search with the initial solution, and finally use the cost value of the best solution found by local search as an upper bound for TT-Open-WBO-Inc. Since the MSE only compares the incomplete solvers using the '#score' metric, we also follow this convention to compare them using this metric.

The results in Table 3 show that SPB-MaxSAT-c outperforms NuWLS-c-2023 in 11 out of 12 benchmarks under 60 seconds of time limit and 8 out of 12 benchmarks under 300 seconds of time limit, indicating that SPB-MaxSAT-c is generally more robust and effective than NuWLS-c-2023. The solvers under 300 seconds of time limit exhibit closer performance because the longer running time of the effective TTOpen-WBO-Inc solver narrows the difference in the performance of the local search algorithms.

5.4 Ablation Study

To analyze the effectiveness and rationality of our proposed adaptive clause weighting strategy, we compare the SPBMaxSAT algorithm with its two variants. The first one simply sets δ = 1, denoted as SPB-MaxSATδ=1, and the second one applies the adaptive clause weighting strategy to both the hard clauses and the SPB constraint, denoted as SPB-MaxSATall. The comparison results of SPB-MaxSAT with these two variants are summarized in Tables 4 and 5, respectively.

The results show that SPB-MaxSAT outperforms SPBMaxSATδ=1, indicating that our adaptive clause weighting strategy is effective and can improve the performance of the clause weighting system. SPB-MaxSAT also outperforms SPB-MaxSATall, indicating that we only highlight the soft clauses and the objective function is reasonable and can lead to better feasible solutions. Using the adaptive clause weighting strategy for both hard clauses and the SPB constraint may make the algorithm swing between hard and soft clauses and cannot focus on improving the objective function so as to find better solutions.

6 Conclusion

Complete algorithm and local search are two research lines of the MaxSAT solvers. Many studies and solvers have tried to apply local search to improve complete solvers, but there have been few attempts in the opposite direction. In this paper, we investigate the utilization of complete solving techniques in improving local search algorithms and focus on the Soft conflict Pseudo Boolean (SPB) constraint widely used in complete solvers to enforce the algorithm to find solutions better than the best solution found so far. We rethink the usage of the SPB constraint and propose integrating SPB into the clause weighting system of local search. We further propose an adaptive clause weighting strategy that allows the dynamic weights to be adjusted proportionally rather than linearly.

Based on the clause weighting techniques, we propose a new local search algorithm, SPB-MaxSAT. Extensive experiments demonstrate its excellent performance and also show that the proposed adaptive clause weighting strategy is reasonable and effective. In future work, we will further investigate the utilization of complete solving techniques for local search and the adaptive clause weighting strategy.

Acknowledgments

This work is supported by National Natural Science Foundation of China (U22B2017) and National Key Laboratory of Electromagnetic Space Security.

Contribution Statement

The first two authors, Jiongzhi Zheng and Zhuo Chen, contributed equally.