From Decimation to Local Search and Back: A New Approach to MaxSAT

1 Introduction

Given a propositional formula expressed in the Conjunctive Normal Form (CNF), the maximum satisfiability problem (MaxSAT) is to find an assignment of Boolean values to the variables of the formula that maximizes the number of satisfied clauses (equally minimizes the number of unsatisfied clauses). MaxSAT is the optimization version of the famous NP-complete problem namely the propositional satisfiability problem (SAT), and has applications in various domains [Xu et al., 2003; Safarpour et al., 2007; Chen et al., 2010; Janota et al., 2012]. An important variant of MaxSAT is the Partial MaxSAT (PMS) problem, in which clauses are divided into hard and soft clauses and the goal is to find an assignment that satisfies all hard clauses and maximizes the number of satisfied soft clauses.

There has been much interest in developing efficient MaxSAT solvers, including both complete solvers and incomplete solvers. A MaxSAT solver is complete if it proves the optimality of the solution it finds when it terminates. Otherwise, it is an incomplete solver. Over the past decade, the most successful approach to solving industrial instances of MaxSAT is the SAT-based approach, which relies on iteratively calling a SAT solver.

∗Corresponding author

For many large industrial instances, because of the NPhardness of the problem and the time constraint, we do not expect to solve them exactly. Instead, the goal is often to find a good-quality solution in a reasonable amount of time. To this end, many incomplete algorithms have been developed.

A main incomplete approach to MaxSAT is local search. Typically, a local search algorithm for MaxSAT starts with a complete assignment, and chooses a variable and flips its value in each subsequent step. The best found assignment is returned when the algorithm reaches its termination condition (e.g., a time limit). Modern local search solvers for MaxSAT [Luo et al., 2015; Cai et al., 2016; Luo et al., 2017] prove efficient in solving random and crafted instances, but their performance on industrial instances is poor.

Another incomplete approach of interest is the decimationbased approach, which proceeds by assigning sequentially the value of some (typically one) of the variables and simplifies the formula accordingly. A main kind of decimation algorithms for satisfiable SAT problems are the message passing algorithms, such as the Survey Propagation (SP) algorithm [Braunstein et al., 2005]. SP has been extended to solve MaxSAT in [Chieu and Lee, 2009]. These algorithms have close connections to statistical physics, and they can be hardly applied to structured instances, mainly because they rely heavily on the statistical properties of solutions [Altarelli et al., 2009]. There are also decimation algorithms based on unit propagation (UP) [Chao and Franco, 1986; 1990; Paturi et al., 2005], which have been studied in the context of SAT and mainly for theoretical interest.

Although various incomplete approaches have been developed for solving MaxSAT, they usually have poor performance on industrial instances. On the other hand, SATbased complete MaxSAT solvers have achieved very good performance on a wide range of industrial instances. This motivates researchers to modify the SAT-based solvers to make them incomplete (i.e., by returning better assignments when found) [Ans´otegui et al., 2016]. Such incomplete solvers dominate the industrial categories of the incomplete track in recent MaxSAT Evaluations (MSEs).

This work proposes a new incomplete approach to efficiently solving MaxSAT. Firstly, we propose a UP-based decimation algorithm for MaxSAT, which, to the the best of our knowledge, is the first UP-based decimation algorithm for MaxSAT. UP-based decimation algorithms have been studied for SAT, and they fail when a conflict is detected. However, when solving MaxSAT, it is unreasonable to stop the decimation procedure upon detecting a conflict, since there are usually unsatisfied clauses under optimal assignments. Instead, in this case, we introduce a heuristic to assign a value to the variable to which the two contradictory unit clause corresponds. When there is no unit clause, we also use the heuristic to assign variables until UP can be applied again.

By combining this decimation algorithm with an existing local search algorithm, we design a solver for MaxSAT named DeciLS.The solver works by interleaving between a decimation procedure and a local search procedure. The assignment produced by the decimation procedure is fed as the initial assignment to local search. More importantly, a feedback mechanism is proposed to provide the best assignment found by the local search procedure to guide the next decimation procedure on assigning variables when UP cannot be applied. We carry out experiments to compare DeciLS against state of the art MaxSAT solvers on all unweighted benchmarks from the MSE 2016 and application formulas from the SAT Competition 2016. The results show that DeciLS has the best performance on all benchmarks except the crafted one. In particular, it outperforms a state of the art SAT-based solver WPM3-2015-in and a recent portfolio solver on all benchmarks, and performs better on industrial benchmark from MSE 2016 and significantly better on the application formulas from the SAT Competition 2016.

Furthermore, we extend our approach to PMS and WPMS, by exploiting the distinction of hard and soft clauses and addressing the issue of no feasible solution found by local search. We implement it with state of the art local search solvers, leading to two hybrid incomplete solvers. Our experiments show that their performance on (W)PMS crafted and industrial benchmarks is significantly better than local search solvers and is complementary and sometime competitive to SAT-based solvers.

The reminder of this paper is organized as follows. The next section introduces the notation and definitions used in the paper. In Section 3, we discuss the related works. We propose our approach in Section 4, and present experimental results of our solver DeciLS in Section 5. Then in Section 6, we extend the approach to (W)PMS and develop two incomplete solvers named DeciDist and DeciCCEHC, and present related experiment results. Finally, we conclude the paper.

2 Preliminaries

Given a set of Boolean variables {x1, x2, ..., xn}, a literal is either a variable x (which is called a positive literal) or its negation ¬x (which is called a negative literal). A CNF formula F is a conjunction of clauses (i.e., F = C1 ∧ C2 ∧ ... ∧ Cm), where a clause is a disjunction of literals (i.e., Ci = ℓi1 ∨ ℓi2 ∨ ... ∨ ℓij). A clause that contains only one single literal is called a unit clause. For a formula F, we denote the set of variables in F by V ar(F).

For a formula 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 unsatisfied if all the literals in the clause are false literals. By convention the empty clause is unsatisfied. The cost of an assignment α (may be partial), denoted by cost(α), is defined to be the number of unsatisfied clauses under α. Given a CNF formula, the MaxSAT problem can be regarded as finding a complete assignment with the minimum cost.

In the Partial MaxSAT (PMS) problem, some clauses are declared to be hard and the rest are declared to be soft, and the task is to find an assignment such that all hard clauses are satisfied and the number of unsatisfied soft clauses is minimized. For a PMS instance F , we say a truth assignment α is feasible iff it satisfies all hard clauses in F, and the cost of a feasible assignment α is defined to be the number of unsatisfied soft clauses under α. In Weighted PMS (WPMS), each soft clause is associated with an integer as its weight, and the cost of a feasible assignment is defined to be the total weight of unsatisfied soft clauses.

The process of conditioning a CNF formula F on a literal ℓ amounts to replacing every occurrence of literal ℓ by the constant true, replacing ¬ℓ by the constant false, and simplifying accordingly. The result of conditioning F on ℓ is denoted by F |ℓ and can be described succinctly as follows: F|ℓ = {c/{¬ℓ}|c ∈ F, ℓ /∈ c} [Darwiche and Pipatsrisawat, 2009]. Note that F|ℓ does not contain any literal ℓ or ¬ℓ. When we assign a variable x with a value v, we can simplify the formula accordingly.

Unit propagation on a CNF formula F works as follows: For a unit clauses in F, the variable is assigned to satisfy this unit clause. That is, if the unit clause {xi} appears in the formula, xi is assigned to true; and if the unit clause {¬xi} appears in the formula, xi is assigned to false. Then the formula is conditioned on this setting. This is a unit propagation step. The iterative execution of such steps until no more unit clause remains is called unit propagation (UP).

3 RelatedWorks

We are not aware of any UP-based decimation algorithm for MaxSAT. Nevertheless, there are a few decimation algorithms for SAT based on unit propagation, which are mainly studied for theoretical interest. An early example is an algorithm called Unit Clause (UC) [Chao and Franco, 1986], which works iteratively until all clauses are satisfied or a conflict is generated. At each step of UC, if there exist unit clauses, a unit clause is picked to perform unit propagation; otherwise, an unassigned variable is selected uniformly at random and is assigned to 1 or 0 uniformly at random. The UC algorithm was extended to the Generalized Unit Clause (GUC) algorithm, where the unassigned variable is always chosen among those appearing in the shortest clauses [Chao and Franco, 1990]. The core of an advanced theoretical SAT algorithm dubbed PPSZ [Paturi et al., 2005] is a UP-based decimation procedure as follows. Take a random order of variables and gradually assign values to them in this order. If a variable currently considered occurs in a unit clause, it is assigned to the value so that the clause is satisfied; otherwise, it is assigned randomly. At each step, if the formula is satisfied, the problem is solved. If two contradictory unit clauses are detected, the decimation procedure stops.

UP has been used in local search for SAT, and in these algorithms (e.g. UnitWalk [Hirsch and Kojevnikov, 2005]), UP is used during local search but not in the generation of initial assignment. Recently, UP was used in generating the initial assignment in local search solvers for PMS [Cai et al., 2016]. The method simply uses UP to produce a partial assignment, and UP stops when no unit clause exists or a conflict is generated. After that, the resulting partial assignment is extended to a complete assignment by assigning all unassigned variables randomly. This initialization process was applied to a local search solver called Dist, leading to an improved solver called DistUP [Cai et al., 2016].

4 ANew Incomplete Approach toMaxSAT

In this work, we propose a new incomplete approach to MaxSAT, with the focus on solving industrial formulas. The proposed approach interleaves between a decimation algorithm and a local search algorithm, with message passing between each other. The process of our approach in a high level is illustrated in Figure 1, and is described below.

The approach works round by round. In each round, an execution of the decimation algorithm produces a complete assignment, which is then handed to the local search algorithm as the initial assignment for possible further improvement. Additionally, a feedback mechanism is employed to provide useful information from local search to the decimation algorithm of the next round. In our approach, the feedback information from local search to decimation refers to the best found assignment during local search of the previous round. However, it could be any information of interest, and the emphasis is on the feedback mechanism rather than the specific feedback information.

The feedback mechanism in our approach is described as follows. The best found assignment in the latest finished local search procedure, denoted by prev ls best, is recorded and maintained, and is used in the decimation procedure. In detail, in the UP-based decimation procedure, if UP cannot be applied, then the variable x under consideration (either it relates to a conflict or it does not appear in a unit clause) is assigned to prev ls best[x].

4.1 The Decimation Algorithm for MaxSAT

In this subsection, we propose a UP-based decimation algorithm for MaxSAT, which is outlined in Algorithm 1. The algorithm works iteratively by assigning variables one by one.

In each step, if there exist unit clauses, the algorithm distinguishes two different cases. If there are not contradictory unit clauses, then it picks a unit clause to perform a unit propagation step. Otherwise, the variable x that relates to two contradictory unit clauses is assigned to the value prev ls best[x], and the formula is simplified accordingly.

If there is no unit clause, then the algorithm picks an unassigned variable x and assigns it to the value prev ls best[x]. The formula is simplified accordingly.

As can be seen from Algorithm 1, we use the pick uc function to pick a unit clause to perform UP, and the pick var function to pick an unassigned variable to assign. Our idea is to employ assigning orders as distant as possible in different rounds of decimation. Firstly, this exploits different reason chains as many as possible, among which the correct (or nearly correct) one may be touched. We believe a key to efficiently solve industrial instances is to find the right reason chain. Secondly, different assigning orders help to generate assignments with large distances in the search space. These solutions are then improved by local search and thus can touch local optima in different areas. Additionally, recalling that our decimation algorithm consults to the best found solution in the last local search procedure, the introduction of this diversification is advisable.

With the above considerations, we utilize a heuristic for both the two functions, which is based on a diversification property. For a variable, we use prev deci step[x] to denote the step number in which it was assigned in the previous round of decimation procedure. For two variables x and y, if prev deci step[x] > prev deci step[y], it means that in the last round of decimation, x is assigned after y.

Our heuristic prefers to pick a variable with a large prev deci step value. We use the Best from Multiple Selection (BMS) strategy [Cai, 2015] for this purpose. In detail, it chooses k variables (k is an integer parameter) randomly with replacement from the set of candidate variables, and returns the one with the greatest prev deci step value. Note that to pick a unit clause among a set of unit clauses, we use the BMS strategy to select the variable from all variables corresponding to unit clauses, and the corresponding unit clause is returned.

4.2 The Local Search Solver

Our approach needs to call a local search solver. Instead of developing a solver from scratch, we modify a local search solver for SAT named CCAnr 1 to make it fit into our approach. As shown in [Cai et al., 2015], CCAnr is amongst the best-performing local search solvers for structured SAT instances. The source code of CCAnr is available online.

In order to integrate CCAnr into our approach, we make a few modifications. Firstly, we add codes to keep track of the best found assignment in each round of local search procedure. Also note that, this data structure is accessible to the decimation algorithm. Secondly, we modify the initialization to make it receive the assignment from the decimation algorithm. Thirdly, each round of local search is stopped if the solution has not been improved in a fixed number of steps (this parameter is denoted as MaxNonImprove). Finally, we remove the "Aspiration" mechanism to make it simpler, as removing it does not have obvious effect.

5 Experiment Evaluation of DeciLS

We conduct experiments to evaluate DeciLS on a broad range of unweighted MaxSAT benchmarks. Experiments show that DeciLS obtains state of the art performance on all benchmarks and performs better than state of the art for the industrial/application instances.

5.1 Experiment Preliminaries

Implementation: DeciLS is implemented in C++ and compiled by g++ with '-O3' option. There are two parameters in DeciLS: parameter k for the BMS heuristic used in the decimation algorithm and MaxNonImprove for local search. We tune these parameters with the automatic configuration tool SMAC [Hutter et al., 2011], and set k = 20 and MaxNonImprove = 50000 for all benchmarks.

Competitors: We compare our solver DeciLS with four state of the art MaxSAT solvers, including WPM3-2015-in [Ans´otegui et al., 2015], CCLS [Luo et al., 2015], MiniWalk [Kroc et al., 2009] and a recent portfolio solver dsat-wpm3in-ms [Ans´otegui et al., 2017]. All these solvers except MiniWalk are the versions submitted to the MSE 2016. MiniWalk is provided by its authors.

1 http://lcs.ios.ac.cn/ caisw/SAT.html

WPM3-2015-in is an incomplete version of the WPM3 solver [Ans´otegui et al., 2015]; it is the best SAT-based incomplete solver for the unweighted MaxSAT industrial category of the MSE2016, and placed 3rd in the category. The portfolio solver dsat-wpm3-in-ms placed 2nd in the category. Note that the winner of this industrial category is an implementation of DeciLS by us. CCLS represents state of the art in local search for unweighted MaxSAT, and has won several categories in recent MSEs, including the incomplete crafted category in MSE 2016. MiniWalk is a hybrid solver that uses a complete SAT solver MiniSAT [E´en and Biere, 2005] to guild a local search solver WalkSAT [Selman et al., 1994] in parallel, and is effective for solving structured MaxSAT instances for which the optimal solutions have only a few unsatisfied clauses [Kroc et al., 2009].

Additionally, to show the complimentary of the solvers, we also report the results of the Virtual Best Solver (VBS), i.e., the perfect selector (not an actual solver) - on each instance, the solution of VBS is the best one of the solutions reported by both solvers; if more than one solver report the best-quality solution, the computing time of VBS is the shortest one.

Benchmarks: We evaluate DeciLS on all random, crafted and industrial benchmarks of unweighted MaxSAT from the MSE2016. Also, we conduct experiments on Application instances from the SAT Competition (SC) 2016, including all formulas that are unsatisfiable (UNSAT), and all those cannot be solved by any solver in the competition (UNKNOWN). These UNSAT and UNKNOWN formulas are a good resource of structured instances for testing MaxSAT algorithms. SAT solvers terminate once they identify a conflict, but MaxSAT solvers can provide useful information. For example, some of these formulas have only a few (even 1) unsatisfied clauses under the optimal solution, and such formulas can be modified to become satisfiable by removing the unsatisfied clauses under the solution.

Experiment setup: All experiments in this work are carried out on a cluster of workstations equipped with Intel Xeon E7-8830 2.13 GHz CPU, 24MB L3 cache and 1.0TB RAM under the operating system CentOS (version: 7.0.1406). Each solver is executed with the runsolver software [Roussel, 2011] for each instance with a cutoff time of 300 seconds (as in the incomplete track of MSEs), and the cost of the best found solution and the time for finding it (the last 'o' line) is recorded. For each solver on each benchmark, we report the number of instances where the solver finds the best solution among all competing solvers in the experiment, denoted by '#win.', and the averaged time of doing so on such winning instances, denoted by 'time' (in CPU seconds).

5.2 Experiment Results on DeciLS

We summarize the experiment results on all unweighted benchmarks in Table 1. DeciLS is overall the best solver on these benchmarks and is particularly effective on the industrial/application benchmarks.

DeciLS is the best solver for all the benchmarks except the crafted benchmark, where it is slightly worse then CCLS. This demonstrates the robustness of DeciLS. Comparatively, other solvers including the portfolio solver have much worse performance than DeciLS on at least three benchmarks.

DeciLS is particularly effective and outperforms its competitors on industrial/application benchmarks. This is remarkable, as industrial benchmarks have been dominated by SAT-based solvers for years. This is the first time a approach that does not call a SAT solver has better performance on such instances. Besides, DeciLS performs very well on also random and crafted instances at the same time, where SATbased solvers are much worse.

5.3 Experiment Analysis on DeciLS

DeciLS combines a decimation algorithm and a local search algorithm CCAnr. In order to show the effectiveness of the cooperation of these two algorithms in the framework, we test two alternatives, denoted as DeciLS onlyDeci and DeciLS onlyLS respectively. DeciLS onlyDeci calls the decimation algorithms iteratively, and records the best found solution. DeciLS onlyLS is indeed the local search solver without modifications made in DeciLS. Since DistUP [Cai et al., 2016] uses UP in the initialization and then performs local search, we also compare DeciLS with DistUP.

Seen from Table 2, DeciLS significantly outperforms the alternatives and DistUP on inudstrial/application benchmarks, while it has almost the same performance with the local search solver on random and crafted benchmarks. The results indicate that the cooperation is critical in our approach, and that the approach is particularly effective for solving industrial instances.

We are also interested in the number of rounds of DeciLS to get the best found solution for each instance. We calculate the averaged number for each MaxSAT benchmark, which are as follows: 1.87 for Random, 7.89 for Crafted, 106.56 for Industrial, and 542.35 for App Unknown, 384.77 for App Unsat.

6 ANew Incomplete Approach to (W)PMS

In this section, we extend our approach to solving (Weighted) Partial MaxSAT. The extension method for WPMS is simply the same one for PMS, and thus we only present the extension to PMS. To extend the approach and make it effective for PMS, some modifications have been carried out as follows:

Firstly, we extend the UP-based decimation algorithm (Algorithm 1) to PMS. When there exist both hard and soft unit clauses, our decimation algorithm for PMS prefers to pick a hard unit clause to perform unit propagation. Similarly, if conflicts are detected, the one that involves hard clauses is addressed first by assigning the corresponding variable according to the heuristic.

Secondly, we must deal with the situation that the previous local search process fails to find a feasible solution. In this case, when UP cannot be performed, the decimation algorithm cannot consult the best found solution by previous local search, and we simply assign the variable randomly.

6.1 Experiments on PMS

We choose Dist [Cai et al., 2016] as the local search solver for PMS in our approach. Dist has been ranked 1st many times in PMS categories of recent MSEs. The resulting hybrid solver is thus named DeciDist. The DeciDist is implemented on the codes of Dist (version 2016), and adopts the default parameter setting there. MaxNonImprove is set to 10000000 for local search in DeciDist. We evaluate DeciDist on all PMS benchmarks in the MSE 2016.

First, we compare DeciDist with two local search PMS solvers namely Dist and DistUP. DistUP improves Dist slightly on PMS industrial instances. The results are reported in Table 3. Compared to the local search solvers, DeciDist has worse performance on PMS random instances. However, DeciDist shows a dramatic improvement over both local search solvers (noting that DistUP uses UP in its initialization) on PMS crafted and industrial benchmarks.

We also compare DeciDist with WPM3-2015-in, which placed 2nd and is the best non-portfolio solver in PMS crafted and industrial categories of the incomplete track in the MSE 2016. We summarize the comparison results in Table 4. Unsurprisingly, the performance of the SAT-based solver WPM3-2015-in is much worse on random instances. On the other hand, WPM3-2015-in has better performance than DeciDist on PMS crafted and industrial benchmarks. Nevertheless, DeciDist still finds better solutions than WPM32015-in for 70 PMS crafted instances and 48 PMS industrial instances. This indicates that Decidist is complementary to WPM3-2015-in on these two benchmarks.

The averaged rounds of DeciDist to get the best found solution for PMS benchmarks are: 1.43 for PMS Random, 6.42 for PMS Crafted and 11.83 for PMS Industrial.

6.2 Experiments onWPMS

We use this approach to improve a state of the art local search solver for WPMS called CCEHC [Luo et al., 2017], resulting in a solver named DeciCCEHC. We first compare DeciCCEHC with CCEHC and CCEHC+UP [Luo et al., 2017], where the later is an improved version of the former by using a UP based initialization as in DistUP. We then compare DeciCCEHC with the SAT-based solver WPM3-2015-in. The experiments are carried out on all WPMS benchmarks in the MSE 2016.

The experiment results for WPMS benchmarks are presented in Tables 5 and 6. Our solver DeciCCEHC outperforms both local search solvers on all WPMS benchmarks, and outperforms WPM3-2015-in on WPMS crafted benchmark, although it is worse on industrial benchmark.

The averaged rounds of DeciCCEHC to get the best found solution for WPMS benchmarks are: 1 for WPMS Random, 1.26 for WPMS Crafted and 113.94 for WPMS Industrial.

7 Conclusions

In this work, we proposed a new incomplete approach to MaxSAT and Partial MaxSAT. The approach is based on a new framework that interleaves between a decimation algorithm and a local search algorithm. We proposed a novel decimation algorithm for MaxSAT which is based on unit propagation, and used it in our framework. The resulting MaxSAT solver named DeciLS showed state of the art performance on random, crafted and industrial benchmarks, and outperforms state of the art SAT-based solvers on industrial benchmarks. We then extended the approach to solving (Weighted) Partial MaxSAT, and the experiments showed that this approach significantly improves the performance of local search on (W)PMS crafted and industrial benchmarks and is complementary to SAT-based solvers.

We believe this new approach is promising for MaxSAT solving and deserves further research. We would like to further improve the approach for (W)PMS problems.

Acknowledgements

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.