Solving (Weighted) Partial MaxSAT by Dynamic Local Search for SAT

1 Introduction

Maximum Satisfiability (MaxSAT) is an optimization version of the famous Satisfiability (SAT) problem. Given a propositional formula expressed in the Conjunctive Normal Form (CNF), MaxSAT concerns about satisfying as many clauses as possible. Partial MaxSAT (PMS) is a generalization of MaxSAT, whose clauses are divided into hard and soft clauses and the goal is to find an assignment that satisfies all the hard clauses and maximize the number of satisfied soft clauses. One can also associate weights to the soft clauses, and the resulting problem is Weighted Partial MaxSAT (WPMS).

PMS and WPMS have many important real world applications, and there is intense interest in developing efficient solvers for these problems. Solvers for (W)PMS can be divided into complete and incomplete solvers. Complete solvers have gain great progress in the last decade. Particularly, a complete method based on iteratively calling a SAT solver, usually referred to as SAT-based method, have attracted much interest. Since its first introduction [Fu and Malik, 2006], many works have been done in improving this method [Davies and Bacchus, 2011; Ans´otegui et al., 2013; Morgado et al., 2013; Martins et al., 2014a; Narodytska and Bacchus, 2014; Ans´otegui and Gab`as, 2017]. SAT-based solvers are especially well known for their good performance on industrial instances. Researchers also modify the complete solvers to make them incomplete (i.e., by returning better assignments when found). The main incomplete method is local search. Local search algorithms maintain a complete assignment and iteratively modify the assignment (i.e., flipping the value of a variable). They keep track of the best solution found throughout the search and return it when reaching the termination condition such as time limit. Local search for (W)PMS has stagnated for years until the recent improvements brought by new techniques [Cai et al., 2014; 2016; Luo et al., 2017; Cai et al., 2017]. Another incomplete method is based on the relation of MaxSAT and the problem of Minimal Correction Subset (MCS) Extraction. It has been shown that restricted enumeration of MCSes is effective at approximating MaxSAT [Marques-Silva et al., 2013; Gr´egoire et al., 2014; Bacchus et al., 2014; Menc´ıa et al., 2015]. Such MCS-based solvers also rely on making calls to complete SAT solvers, but they are usually less effective than the SAT-based solvers on structured instances.

∗Corresponding author

Local search is essentially an anytime method and is particularly suitable for real domains where we are often interested in getting a good-quality solution within reasonable time. In many problem domains of combinatorial optimization, local search is widely acknowledged as one of the most effective methods for solving large instances, including those from real world applications. Comparatively, the way of local search for (W)PMS is more difficult and is more interesting, mainly due to the problem feature. Local search has witnessed its success on solving random and some crafted benchmarks, but it has been criticized for its poor performance on industrial instances for a long time. Recently, Cai et. al. firstly developed a local search solver that achieves state of the art performance when compared with complete MaxSAT solvers on unweighted MaxSAT industrial instances [Cai et al., 2017]. Improvements have also been made on improving local search for

(W)PMS industrial instances, but the gap between the performance of local search and complete solvers is still considerably large on such benchmarks.

Related works in local search for (W)PMS can be categorized into two lines. Early studies belong to the first line, and these algorithms encode (W)PMS as weighted MaxSAT by introducing a hard clause multiplier, such that the weighted cost of a hard clause is the product of the multiplier and the actual weight currently added to the clause. The focus of this line is to set an appropriate value to the multiplier, which can be done statically [Cha et al., 1997; Luo et al., 2015] or dynamically [Thornton and Sattar, 1998; Thornton et al., 2002]. Such solvers do not sufficiently exploit the structure of (W)PMS and has poor performance. Recent studies on specialized local search for (W)PMS emerge as the second paradigm. These local search algorithms introduce the concepts of hard score and soft score [Cai et al., 2014], and employ different heuristics for hard and soft clauses respectively. The resulting solvers, including Dist [Cai et al., 2014] and CCEHC [Luo et al., 2017], as well as their improved versions [Cai et al., 2016; 2017], made significant improvements over previous local search solvers. However, they are more complicated with the concepts and heuristics tailored for hard and soft clauses separately.

In this work, we propose a novel local search algorithm for (W)PMS, which adopts a dynamic local search framework for SAT and exploits the distinction of hard and soft clauses by a carefully designed clause weighting scheme. Briefly speaking, the weighting scheme updates weights for both hard and soft clauses, while it puts more increments to hard clauses each time and also sets a limit on the maximum weight that each soft clause can get. It is interesting to note that, previous local search algorithms for (W)PMS did not benefit that much from the techniques for SAT [Cai et al., 2016]. One may consider that due to some reasons, e.g., (W)PMS contains hard and soft clauses, local search for SAT is not suitable for solving (W)PMS. In this work, we show that how local search techniques for SAT can be used for effectively solving (W)PMS. Our algorithm is thus called SATLike. According to experiments on PMS and WPMS benchmarks, SATLike significantly improves the state of the art of local search for (W)PMS on all benchmarks. Further, SATLike significantly narrows the gap between local search and complete solvers on industrial instances. Note that, these achievements are obtained by using simple concepts already used in local search for SAT.

The reminder of this paper is organized as follows. The next section introduces preliminary knowledge. We introduce our main ideas in Section 3. Then, we present our SATLike algorithm for (W)PMS in Section 4. Experimental results of our solver are presented in Section 5. Finally, we conclude the paper.

2 Preliminaries

Given a set of Boolean variables{x1, x2, x3, . . . , xn}, a literal is either a variables xi or its negation ¬xi. A clause is a disjunction of literals (i.e., Ci = li1 ∨ li2 ∨ · · · ∨ lij). A

conjunctive normal form (CNF) formula F is a conjunction of clauses (i.e., F = C1∧C2∧· · ·∧Cm), and can be expressed as a set of clauses.

For a formula F, the set of variables appeared in F is denoted by V ar(F ). An assignment α is a mapping V ar(F ) → {0, 1}. A complete assignment is a mapping that assigns to each variable either 0 or 1. A clause is satisfied if it has at least one true literal, and falsified if all the literals in the clause are false literals.

Given a CNF formula, the Partial MaxSAT (PMS) problem, in which some clauses are declared to be hard and the rest are declared to be soft, is the problem of finding an assignment such that all hard clauses are satisfied and the number of satisfied (resp. falsified) clauses is maximized (resp. minimized). In Weighted PMS (WPMS), each soft clause is associated with a positive integer as its weight, and the goal is to satisfy all hard clauses and maximize the total weight of satisfied soft clauses.

For a (W)PMS instance F , we say an assignment α is feasible iff it satisfies all hard clauses in F . The cost of a feasible assignment α is defined to be the number (resp. the sum of original weights) of falsified soft clauses under α for PMS (resp. WPMS). For convenience, the cost of any infeasible assignment is defined to be +∞.

Local search algorithms for SAT and MaxSAT problems, including (W)PMS, maintain an assignment and modify it iteratively. Specifically, starting with a complete assignment, a local search algorithm chooses a variable and flips it in each subsequent step, trying to find a feasible assignment with a lower cost. Local search algorithms with clause weighting techniques modify the weights of clauses during the search, and are also called Dynamic Local Search (DLS). To distinguish the original weight and the weight maintained by clause weighting techniques, we use org w(c) to denote the former, and w(c) the latter. Local search algorithms use scoring functions and heuristics to guide the search. The most common used scoring function is perhaps the score of variables.

Definition 1 (Score in DLS) In dynamic local search algorithms, the score of a variable x, denoted by score(x), is the increase of total weight of satisfied clauses caused by flipping x.

Definition 2 (Decreasing variable) A variable x is decreasing iff score(x) > 0 (as its flip would decrease the cost).

Although the score of variables have been widely used in local search for SAT and non-partial MaxSAT, its use in (W)PMS is not straightforward, due to the distinction between hard and soft clauses. Recent local search algorithms for W(PMS) also utilize the notion of hard score and soft score, which is the version of score limited to hard and soft clauses respectively.

3 Main Ideas

In this section, we present the two main new ideas in our algorithm.

3.1 NewWeightingMechanism

In this subsection, we propose a new clause weighting scheme for (W)PMS, which works on both hard and soft clauses while at the same time takes into account the distinction between hard clauses and soft clauses. This is essentially different from previous clause weighting schemes for (W)PMS, which either do not distinguish hard and soft clauses [Thornton et al., 2002; Luo et al., 2015] or just works on hard clauses [Cai et al., 2014; Luo et al., 2017].

Our clause weighting scheme is named Weighting-PMS, and works as follows. For each hard clause, we associate an integer number as its weight which is initialized to 1; for each soft clause, we use the original weight (which is 1 for PMS, and is the original weight from the input file for WPMS) as its initial weight. Whenever a "stuck" situation is observed, that is, we cannot decrease the cost by flipping any variable, then clause weights are updated as follows.

• with probability 1 - sp: for each falsified hard clause c, w(c) := w(c) + h inc; for each falsified soft clause c, w(c) := w(c) + 1 if w(c) < ζ.
• with probability sp (smoothing probability): for each satisfied hard clause c s.t. w(c) > 1, w(c) := w(c) - h inc; for each satisfied soft clause c s.t. w(c) > 1, w(c) := w(c) -1.

Our weighting scheme is the first one that works on both hard and soft clauses while at the same time distinguishes hard and soft clauses. The way for updating clause weights are similar to PAWS [Thornton et al., 2004]. Some discussions on the ideas are presented below.

Insights on heavy weighting for hard clause are given below. It is natural to perform clauses weighting for hard clauses, as all hard clauses must be satisfied, and clause weighting helps to identify those difficult hard clauses that are usually falsified in local optima so that the algorithm prefer to satisfy them. Indeed, the intuition here is similar to clause weighting for SAT.

Further, by giving a higher weight increment (h inc ≥ 1) to falsified hard clauses than soft ones, it helps to highlight the hard clauses. In this way, the algorithm prefers to satisfy hard clauses, which is the primary objective of the problem.

Insights on light weighting for soft clause are given below. One can view all soft clauses as a non-partial formula, and by updating weights for soft clauses, we try to satisfy as many soft clauses as possible. Indeed, this is what local search for non-partial MaxSAT usually does [Hoos and St¨utzle, 2005]. Recent specialized local search algorithms for (W)PMS [Cai et al., 2014; Luo et al., 2017] (Dist and CCEHC) do not update clause weights for soft clauses, as they concern about the possible misleading by weighting for soft clauses.

In our mechanism, we avoid such misleading in two ways. We set a higher weight increment to hard clauses, while the increment is set as 1 for soft clauses. Also, we set a limit on the maximum value of soft clause weight. As is usually the case, there are some soft clauses falsified under optimal assignments. If the weights of soft clauses can grow arbitrarily, such soft clauses would have very high weight, and would prevent us from finding feasible solutions. To avoid this situation, giving a control to the maximum value of soft clause weights is necessary.

3.2 Variable Selection Heuristic

This subsection proposes a novel variable selection heuristic. We design a new variable selection heuristic, which adopts a two-mode dynamic local search framework and exploits the double-make variables. In details, the variable to be flipped is picked as follows:

Firstly, if there exist decreasing variables, the algorithm picks one of the decreasing variables. Observe that for some instances, the number of candidate variables here might be very large, so we use a probabilistic sampling strategy named "best from multiple selections" (BMS) [Cai, 2015] to pick a decreasing variable with high score. Specifically, the algorithm chooses t random variables (with replacement), and returns the one with the highest score. This BMS strategy has proved effective for improving local search on large scale instances, in that it can return an element with very good quality with a constant number of samples. For example, according to calculations in [Cai, 2015], 50 samples guarantees that the returned variable's score is at 10% top among all decreasing variables.

Secondly, if there are no decreasing variables: This means the search gets stuck, as no improving flip is available. In this case, the clause weights are updated, and then a variable in a falsified clause is picked. Since all hard clauses must be satisfied, we select a random falsified hard clause if any, and otherwise a random falsified soft clause will be selected. After the falsified clause is selected, the one with the greatest score is picked. Ties are broken by preferring the variable that is least recently flipped.

4 The SATLike Algorithm

In this section, we present our local search algorithm for (W)PMS, which uses similar techniques in local search for SAT, and thus is called SATLike.

In the beginning, SATLike generates a complete assignment α, and the best found solution α∗ is initialized as ∅. We use the initialization procedure based on unit propagation [Cai et al., 2017] to produce an initial complete assignment for PMS, while the UP-based initialization is not useful for SATLike on WPMS and so the initial assignment is generated randomly for WPMS.

After that, a loop (lines 3-15) is executed to iteratively modify α until a given time limit is reached. During the search, whenever a better feasible solution is found, the best feasible solution α∗ , and cost∗ , are updated accordingly (line 4). At each iteration, SATLike chooses a variables and flips it, according to the variable selection heuristic introduced in the previous section.

If the set of the decreasing variables D is not empty, SATLike picks a decreasing variable with the greatest score from t samples with replacement fromD, breaking ties by preferring the one that is least recently flipped.

If there is no decreasing variable, which means the search get stuck, then SATLike updates clause weights according to the Weighting-PMS scheme described in the preceding section, and picks a variable from a falsified clause. Specifically, it chooses a clause randomly from falsified hard clauses if

Algorithm 1: SATLike

any, and from falsified soft clauses otherwise. Then, SATLike picks the variable with the greatest score in the clause.

Finally, when the loop terminates upon reaching the time limit, SATLike returns cost∗ and α∗ if α∗ is a feasible solution. Otherwise, it returns "no feasible assignment found".

5 Experimental Evaluation of SATLike

We evaluate SATlike on (W)PMS benchmarks from the MaxSAT Evaluation (MSE) 2016 and 2017, compared with state of the art local search and SAT-based solvers.

5.1 Experiment Preliminaries

We evaluate SATLike on all benchmarks of PMS and WPMS problems from the MaxSAT Evaluations (MSE) 2016 and 2017. In MSE 2016, there are 3 PMS benchmarks and 3 WPMS benchmarks, for random, crafted and industrial categories respectively, while MSE 2017 merged all PMS categories into a benchmark (PMS 2017), and all WPMS categories into a benchmark (WPMS 2017).

SATLike is implemented in C++ and compiled by g++ with '-O3' option. There are 4 parameters in the SATLike solver:

• t: the number of samplings, used in the BMS heuristic
• sp: the smooth probability, used inWeighting-PMS
• h inc: the increment for each falsified clause each time, used in Weighting-PMS
• ζ: the limit on maximum value on soft clause weight, used in Weighting-PMS

The parameters are tuned according to our experience, and are listed as followed:

For PMS Random and PMS Crafted benchmark: t=15,sp=0.01,h inc=2,ζ=1;

For PMS Industrial and PMS 2017 benchmarks: t=42,sp=0.000003,h inc=1,ζ=400;

For WPMS Random and WPMS Crafted benchmark: sp=0.01;

For WPMS Industrial and WPMS 2017 benchmarks: sp=0.0001;

For all WPMS benchmarks: t=15; h inc=300 and ζ=500 iff soft clause average weight > 10000, otherwise h inc=3 and ζ=1;

We compare SATLike with local search solvers. For PMS benchmarks, we choose the local search solver Dist (version 2016) and its latest improved version DeciDist [Cai et al., 2017]. For WPMS benchmarks, we choose the local search solver CCEHC [Luo et al., 2017] and its latest improved version DeciCCEHC [Cai et al., 2017]. DeciDist and DeciCCEHC are the best local search solvers for PMS and WPMS respectively. Also note that the parameters of these local search solvers have been tuned for each (W)PMS benchmark from MSE 2016, and we use these parameter settings for each benchmark as reported in their papers [Cai et al., 2016; Luo et al., 2017].

We compare with three state of the art complete solvers. WPM3 is a famous SAT-based solver and was ranked first in both complete and incomplete tracks in recent MaxSAT Evaluations, including the crafted and industrial categories of PMS and WPMS. Open-WBO [Martins et al., 2014b] is also a SAT-based complete solver, and won the PMS crafted category of MSE 2016 and unweighted complete track of MSE 2017. MaxHS [Davies, 2013] is a SAT-based solver and won the WPMS crafted and industrial categories of MSE 2016 and weighted complete track of MSE 2017. For our experiments, we use the version of WPM3 submitted to incomplete track of MSE 2016 and 2017 (WPM3-in), and the latest release version online for Open-WBO (version 2017.10) and MaxHS (2016). WPM3-in and OpenWBO refine upper bounds during the search, and once a better solution is found, it is printed. But MaxHS only prints the result when it finishes, so the results of MaxHS are only for reference.

Our experiments were conducted on a workstation using an Intel(R) Core(TM) i7-4710MQ CPU with 2.50GHz, 4MB L3 cache and 16 GB RAM, running Ubuntu 14.04 Linux operation system. Each solver is executed once on each instance within 300 seconds (as in MSEs). In each run, the solver prints successively the best solution it has found so far. For each solver on each instance family, we report the number of instances where the solver finds the best solution among all solvers in the table, denoted by "#win." and the mean time of doing so over such "winning" instances (not including the proving time for complete solvers). The number of instances of each family is specified in the column "#ins.". The rules at the MaxSAT Evaluations establish that the winner is the solver which finds the best solution for the most instances and ties are broken by selecting the solver with the minimum mean time. In bold we present the best results for each family.

5.2 SATLike vs. Local Search Solvers

In this subsection, we compare SATLike with state of the art local search solvers. We firstly compare SATLike with Dist and DeciDist on PMS benchmarks. The results are summarized in Table 1. SATLike is the best solver on all the PMS benchmarks, and it significantly outperforms Dist and DeciDist on crafted and industrial PMS benchmarks. The number of winning instances for SATlike is about 1.1 and 2.3 times that for DeciDist on the crafted and industrial PMS benchmark respectively.

Experiment results on comparing SATLike with state of the art local search solvers for WPMS (namely CCEHC and DeciCCEHC) are presented in Table 2. SATLike outperforms CCEHC and DeciCCEHC on all WPMS benchmarks, and obtains remarkable improvements over them on crafted and industrial benchmarks. In particular, for the WPMS industrial benchmark, the winning instances for SATLike is 525, compared to 101 and 56 for CCEHC and DeciCCEHC, which indicates a dramatic improvement.

5.3 SATLike vs. Complete Solvers

We also compare SATLike with three state of the art complete solvers. In Table 3 we summarize the experiment results on comparing SATLike and complete solvers on all benchmarks, and we have the following observations.

SATLike is significantly better than complete solvers on random benchmarks. For crafted benchmarks, SATLike and complete solvers are competitive with each other: complete solvers are better on PMS crafted benchmark while SATLike are better on WPMS crafted benchmark.

For industrial benchmarks, SATLike cannot compete with the complete solvers yet. Nevertheless, the results are still encouraging. The number of winning instances for SATLike achieves about 66% and 72% that for the best complete solver for PMS and WPMS industrial benchmarks respectively, which is a gap that previous local search solvers can hardly reach.

We are also encouraging to see that, for 2017 benchmarks, SATLike is much better than all the complete solvers. These results show the overall strong performance of SATLike on (W)PMS benchmarks.

To gain a more detailed comparison between SATLike and the complete solvers on industrial benchmarks, we present the results on each instance class, as shown in Table 5 and 6. The results show that, SATLike is complementary to the complete solvers on these industrial benchmarks.

5.4 Experimental Analysis on SATLike

To show the effectiveness of the clause weighting scheme in SATLike, we test two alternatives of SATLike, which replace the Weghting-PMS scheme with its variants. The first one SATLike alt1 uses the clause weighting scheme without threshold of soft clauses weight. The second one SATLike alt2 adds the same increment (that is one) for falsified hard and soft clauses. Experiment results show that SATLike significantly outperforms these two alternatives on all the benchmarks (Table 4). This demonstrates the WeightingPMS scheme in this work plays a key role in SATLike.

6 Conclusions and FutureWork

In this work, we proposed to solve the (weighted) partial MaxSAT problem by dynamic local search techniques from SAT background. The strong results show that local search techniques for SAT can be useful to solve (W)PMS problems. Our main idea is a novel clause weighting scheme that works differently for hard clauses and soft clauses. The resulting solver SATLike dramatically outperforms previous local search algorithms on PMS and WPMS benchmarks. Further, when compared to state of the art complete MaxSAT solvers, SATLike is complementary and has better performance on the benchmarks from MSE 2017. Our work significantly narrows the gap between the performance of local search and the currently best approach on the industrial benchmarks.

This work opened a new local search direction for (W)PMS, which is promising to efficiently solve (W)PMS structured instances. We would like to use more advanced local search methods in SAT to enhance our algorithm.

Acknowledgement

This work is supported by National Natural Science Foundation of China 61502464, China National 973 Program 2014CB340301. Shaowei Cai is also supported by Youth Innovation Promotion Association, Chinese Academy of Sciences.