Keywords

1 Introduction

Given a set of Boolean constraints in a conjunctive normal form (CNF), the problem of Maximum Satisfiability (MaxSAT) asks to provide valuation of variables so that maximum number of constraints are satisfied. These constraints can be assigned weights to prioritize some set of constraints over others, which would give rise to a weighted MaxSAT problem where the goal is to find a valuation which maximizes the sum of the weights of the satisfied constraints. Any improvements in MaxSAT solving have a huge impact because many real world problems can be encoded as MaxSAT problems (e.g., [5, 14, 16]).

Often, the application may be able to tolerate a suboptimal solution but requires this solution to be computed in a very short amount of time. For such cases, it tremendously helps if there are techniques and tools that can very quickly find a solution which is close enough to an optimal solution. Incomplete MaxSAT solvers [4, 9, 10, 19, 20, 26] strive to find a good solution in a limited time frame. The solution, thus provided, need not be an optimal one. Therefore, for improvement, we need to develop tools and techniques that can find better solutions (closer to an optimal solution) in the same time frame.

As part of this paper, we contribute the following:

  • An approximation strategy based on weight relaxation (Sect. 3), which modifies the weights of the clauses in a manner so that it is easier for the solver to find a solution quickly.

  • An approximation strategy which breaks up the problem of minimizing the sum of weights of unsatisfied clauses into multiple minimization subproblems and attempts to minimize these subproblems in a greedy order (Sect. 3). This strategy can also be combined with the weight relaxation strategy.

  • Empirical results on how the accuracy of the solver gets affected as we vary the weight relaxation parameter (Sect. 5).

  • An implementation of these strategies using the Open-WBO framework. We also demonstrate the advantage of these approximation strategies by showing its prowess against state-of-the-art incomplete MaxSAT solvers (Sect. 5).

2 Preliminaries

Let x be a Boolean variable which can take values \( true \) or \( false \). A literal l is a variable x or its negation \(\lnot x\). A clause \(\omega \) is a disjunction of literals and a formula \(\varphi \) is a conjunction of clauses. Notationally, we will treat a clause \(\omega \) and a formula \(\varphi \) as sets containing literals and clauses respectively.

An assignment \(\nu \) maps variables to either \( true \) or \( false \). An assignment is said to satisfy a positive literal x (resp. a negative literal \(\lnot x\)) if \(\nu (x)= true \) (resp. \(\nu (x)= false \)). A clause is said to be satisfied if at least one of its literals is satisfied. A formula is said to be satisfied by an assignment if all of its clauses are satisfied by the assignment. A formula is called satisfiable if there exists a satisfying assignment for that formula, otherwise it is called unsatisfiable. Boolean satisfiability problem (SAT) asks to find a satisfying assignment (i.e., model) to a formula. Maximum satisfiability (MaxSAT) problem is an optimization version where the goal is to find an assignment which satisfies the maximum number of clauses of a formula. In a partial MaxSAT problem, a partition of \(\varphi \) is given as two mutually exclusive sets \(\varphi _h\) (hard clauses) and \(\varphi _s\) (soft clauses), where the goal is to satisfy all the clauses in \(\varphi _h\)Footnote 1 while maximizing the number of clauses satisfied in \(\varphi _s\). Let \(weight:\;Clauses \rightarrow \mathbb {N}^{+}\) be a map from a set of clauses to positive integers. In a partial weighted MaxSAT problem, the goal is to find an assignment that maximizes the sum of weights of the satisfied soft clauses. From now on, we will refer to a weighted partial MaxSAT problem as MaxSAT.

A clause \(\omega \) can be relaxed by adding a relaxation variable r so that the relaxed clause becomes \(\omega \cup \{r\}\). The relaxed clause can be satisfied by either satisfying the original clause or its relaxation variable. For a formula \(\varphi \), when all of its soft clauses are relaxed, we will denote it as \(\varphi ^r\). We define the cost of a relaxation variable r to be the weight of the clause that it relaxed, \(cost(r)=weight(\omega )\). The cost of an assignment \(\nu \) is defined as \(cost(\nu )=\sum _{r_i:\nu (r_i)=1} {cost(r_i)}\). The goal of MaxSAT is to find a satisfying assignment with the minimum cost.

3 Approximation Strategies

In this section, we describe two approximation strategies that can allow MaxSAT algorithms to converge faster to lower cost solutions. Note that the best model found by approximation strategies is not guaranteed to be an optimal solution of the original MaxSAT formula.

Weight-Based Approximation. Let \(P_m(\varphi _s)=\{c_1,\dots ,c_m\}\) be a partition of \(\varphi _s\) into m mutually exclusive sets \(c_1,\dots ,c_m\) such that \(\bigcup _{ 1 \le i \le m} c_i = \varphi _s\) and \(\forall _{i\ne j} : c_i \cap c_j = \emptyset \). We will call sets \(c_1,\dots ,c_m\) as clusters of the partition.

figure a
figure b

Given a formula \(\varphi _s\), Algorithm 1 partitions the clauses into clusters as follows. All soft clauses are sorted by their weights (Line 2). Then, differences in weights between two consecutive clauses are calculated (Line 4). \(m-1\) indices are picked where the weight differences are amongst the top \(m-1\) weight differences (Line 5). These indices are used as boundaries to create clusters (Lines 6–9). This way of clustering is similar to single-link agglomerative clustering [15]. Finally, a new weight map \(weight_m\) is created, where all the clauses in the same cluster get the same weight (Lines 11–13). RepresentativeWeight (Line 13) indicates any representative weight for the cluster. In this paper, we use the arithmetic mean of the weights of the clauses in a cluster as the representative weight. In principle, other representative weights can also be chosen which may have different effect on how much an algorithm can deviate from finding the minimum cost assignment. It is redundant to have \(m>\#weights\), where \(\#weights\) are different number of weights, because for \(m\ge \#weights\), \(weight=weight_m\). Algorithm 1 can be combined with any search algorithm and as m increases the deviation of the search algorithm from an optimal solution decreases. If \(m=0\) it is assumed that no partitioning is done.

There are encodings which perform better when \(\#weights\) is small [12, 17]. Such encodings can benefit from approximation of weights because it results in a smaller size formula when converted to CNF. This can be used with a cost minimization algorithm for MaxSAT such as the linear search Sat-Unsat algorithm [8, 18] shown in Algorithm 2. In this algorithm, all the clauses in \(\varphi _s\) are initially relaxed, and the set of corresponding relaxation variables is denoted as \(V_R\). A working formula \(\varphi _W\) is initialized with the relaxed formula \(\varphi ^r\). The cost of an empty model is assumed to be \(+\infty \). Our primary goal is to find a satisfying assignment \(\nu \) to \(\varphi \) with the minimum \(cost(\nu )\). Algorithm 2 iteratively asks a SAT solver if there is a satisfying assignment, with its cost at most \(\mu -1\) (Line 9). The approximation comes from Algorithm 2 using \(cost_m\) instead of cost to encode a pseudo-Boolean (PB) constraint that restricts the cost of relaxation variables being set to \( true \) (Line 9). Since \(cost_m\) is an approximation of cost, minimizing \(cost_m\) does not necessarily translate to minimization w.r.t. cost. Therefore, we update model, only when a satisfying assignment indeed reduces the previous value of \(cost(\mathsf {model})\) (Lines 6–7).

figure c

Approximation via Subproblem Minimization. Algorithm 3 proceeds in a greedy manner by processing each cluster in the descending order of its representative weight (Line 2). \(V_i\) indicates a set of relaxation variables corresponding to the clauses in \(c_i\) (Line 3). Minimization of the cost of a satisfying assignment is divided in subproblems by minimizing the number of unsatisfied clauses in clusters, starting from highest representative weight to the lowest (Line 2). For each cluster, the number of unsatisfied clauses are minimized by iteratively reducing the upper bound \(\mu _i\) on the number of relaxation variables in \(V_i\) that can be set to \( true \) (Lines 10–11). In the process, the minimum cost assignment seen so far is recorded (Lines 8–9). Since within any cluster, all the clauses have the same \(weight_m\), only cardinality constraints are used to restrict the number of unsatisfied clauses within \(\mu _i\) (Line 11). Once \(\mu _i\) can not be reduced further, it is frozen by adding upper bound \(\mu _i\) for all the cluster seen so far (Lines 12–15). Since the minimization is done locally as a minimization subproblem at a cluster level, rather than looking at the whole formula, this procedure is not guaranteed to converge to a globally optimum solution.

4 Related Work

Approaches for incomplete MaxSAT solving can primarily be divided into two categories: (i) stochastic MaxSAT solvers [9, 10, 13, 19, 20] and (ii) complete MaxSAT solvers that can find intermediate solutions [4, 8, 11, 18, 23, 25].

Incomplete MaxSAT. Stochastic solvers start by finding a random assignment \(\nu \) for \(\varphi \). Since this assignment is unlikely to satisfy all clauses in \(\varphi \), they choose a clause \(\omega _i\) that is unsatisfied by \(\nu \) and flip the assignment of a variable in \(\omega _i\) such that \(\omega _i\) becomes satisfied. When compared to local SAT solvers, stochastic MaxSAT solvers have additional challenges since they must find an assignment \(\nu \) that satisfies \(\varphi _h\) while attempting to minimize the cost of the unsatisfied soft clauses. Stochastic MaxSAT solvers are particularly effective for random benchmarks but their performance tends to deteriorate for industrial benchmarks. Since the MaxSAT Evaluation 2017 (MSE2017) [2] did not contain any random instances, there were no stochastic MaxSAT solvers in the MSE2017.

Complete MaxSAT. Complete solvers can often find intermediate solutions to \(\varphi \) before finding an optimal assignment \(\nu \). MaxSAT solvers based on linear search algorithms [8, 18, 23] can find a sequence of intermediate solutions that converge to an optimal solution. These solvers use PB constraints to enforce convergence. While SAT4J [8] uses specialized data structures for PB constraints to avoid their conversion to CNF, other solvers such as QMaxSAT [18] convert the PB constraint into clauses using PB encodings [12, 17, 27]. Some MaxSAT solvers which are based on the implicit hitting set approach [11, 25] maintain a lower and an upper bound on the values of the solution. These solvers can also be used for incomplete MaxSAT since they are also able to find intermediate solutions. Another approach for complete MaxSAT solving is to use unsatisfiability-based algorithms [1, 4, 24]. These algorithms use unsatisfiable subformulas to increase a lower bound on the cost of a solution until they find an optimal solution. For weighted MaxSAT, these algorithms employ a stratified approach [3] where they start by considering only a subset of the soft clauses with the largest weights and iteratively add more soft clauses when the subformula becomes satisfiable. An intermediate solution is found at each iteration. WPM3 [4] is an example of an unsatisfiable-based solver that can be used for incomplete MaxSAT and was the best incomplete MaxSAT solver in the MSE2016 [6]. maxroster [26] was the winner of the incomplete track for Weighted MaxSAT in the MSE2017. It is a hybrid solver that combines an initial short phase of a stochastic algorithm [13] with complete MaxSAT algorithms [18, 24].

Boolean Multilevel Optimization. The clustering-based algorithm presented in Algorithm 3 is closely related to Boolean Multilevel Optimization (BMO) [21]. BMO is a technique for identifying lexicographic optimization conditions, i.e. the existence of an ordered sequence of objective functions. Let \(M_i\) be the minimum weight of soft clauses in a cluster \(c_i\). Consider a sequence of clusters \(c_1, \ldots , c_m\) arranged in a descending order of \(M_i\). A MaxSAT formula is an instance of BMO if for every cluster \(c_i\), \(M_i\) is larger than the sum of the weights of all soft clauses in clusters \(c_{i+1}, \ldots , c_m\). If this condition holds then the result of Algorithm 3 is equivalent to solving a BMO formula. However, when using the proposed clustering-based algorithm on partitions that do not preserve the BMO condition, it is not guaranteed that the solution found by Algorithm 3 is an optimal solution for \(\varphi \). Our approach differs from previous complete approaches in using approximation strategies that do not preserve optimality but are more likely to converge faster to a better solution.

5 Experimental Results

To evaluate incomplete MaxSAT solvers we used the scoring mechanism from MaxSAT Evaluations 2017 (MSE2017) [2]. Given a formula \(\varphi \), the score for a solver \(\mathcal S\) is computed by the ratio of the cost (sum of weights of unsatisfied clauses) of the best solution known for \(\varphi \), denoted as \(best(\varphi )\),Footnote 2 to the best cost found by \(\mathcal S\), denoted as \(cost^{\mathcal S}(\varphi )\).Footnote 3 The score for \(\mathcal S\) for a set of n benchmarks is given by the average score ([0, 1]) as follows:

$$\begin{aligned} \mathsf{score}(\mathcal S) = \frac{\sum _{i=1}^n\frac{best(\varphi _i)}{cost^{\mathcal S}(\varphi _i)}}{n} \end{aligned}$$
(1)

score(\(\mathcal S\)) shows how close on average is a solver S to the best known solution.

All the experiments were conducted on Intel® Xeon® E5-2620 v4 processors with a memory limit of 32 GB and time limits of 10, 60 and 300 s. We have used a non-standard timeout of 10 s to show that approximation strategies can find good solutions very quickly. We used the 156 benchmarks for incomplete MaxSAT from MSE2017 [2]. Note that most of these benchmarks are challenging for complete solvers and have unknown optimal solutions.

We have implemented all the algorithms presented in this paper in Open-WBO-Inc. Open-WBO-Inc is built on top of Open-WBO [23] which uses Glucose [7] as the underlying SAT solver. We used Generalized Totalizer Encoding (GTE) [17] and incremental Totalizer encoding [22] to translate PB constraints and cardinality constraints into CNF, respectively.

We evaluated Open-WBO-Inc by conducting experiments that are designed to answer the following questions: (1) What is the impact of the number of clusters in the quality of the solution found by our approximation strategies? (2) How does Open-WBO-Inc compare against state-of-the-art incomplete MaxSAT solvers?

Impact of the Number of Clusters. We measure the impact of partitioning parameter m on the accuracy of the results. Figure 1a shows the score of Algorithm 2 with GTE encoding (henceforth called apx-weight). Figure 1a shows that apx-weight performs the worst when no partitioning is done. This is attributed to the fact that in the absence of any partitioning, the size of the underlying encoding is dictated by \(\#weights\), where \(\#weights\) are the number of different weights in the weight map. Figure 1c shows a measure of increase in formula size as m varies. The Y-axis shows the ratio of the formula size after the PB encoding to the size of the original input formula. Because of the weight-based approximation, the reduction on the \(\#weights\) leads to a smaller encoding, thus making it easier for the underlying SAT solver. As m increases, the possible deviation from an optimal cost also decreases, thereby resulting in increased scores. The degradation for larger m is attributed to larger size of the formula. As the timeout is increased, the score increases because Algorithm 2 has more time and can do more iterations to reduce \(cost_m(\mathsf {model})\).

Figure 1b shows that similar scoring trends are witnessed for Algorithm 3 (henceforth called apx-subprob). As apx-subprob uses only cardinality constraints, the formula size is not much sensitive to m. As m increases, the scores also improve, with the best scores achieved when \(m=\#weights\). apx-subprob is guaranteed to find optimal solution only if BMO condition holds and \(m=\#weights\). Only 3 out of 156 benchmarks have the BMO condition and apx-subprob with \(m = \#weights\) does not terminate for any of them. However, apx-subprob using a 300 s time limit terminates for 94 out of 156 benchmarks which shows that apx-subprob quickly finds a good solution.

Comparison Against State-of-the-Art MaxSAT Solvers. We compared the best version of Open-WBO-Inc for weight-based approximation, apx-weight with \(m=2\), and subproblem minimization approximation, apx-subprob with \(m=\#weights\), with maxroster [26], WPM3 [4] and QMaxSAT [18]. maxroster and WPM3 were the winners of the incomplete weighted category of the MSE2017 and MSE2016, respectively. QMaxSAT was placed second on the complete category of the MSE2017 and uses the algorithm described in Algorithm 2.Footnote 4

As shown in Fig. 1d, for a 10 s timeout, both apx-weight and apx-subprob perform better than all the other solvers with apx-subprob performing the best. This demonstrates that approximation strategies are quite effective when we want to quickly find a solution which is closer to an optimal solution. For 60 and 300 s timeout, apx-subprob performs the best with maxroster being second and apx-weight outperforming WPM3 and QMaxSAT. Even though apx-weight with \(m=0\) performs worse than QMaxSAT, it outperforms QMaxSAT when clustering is used. apx-subprob outperforms all other solvers and these results prove the efficacy of approximation strategies with respect to the state-of-the-art in incomplete MaxSAT solving.

Fig. 1.
figure 1

Impact of clustering and comparison against state-of-the-art

Full size image

6 Conclusion and Future Work

Approximation strategies, be it weight-based relaxation or subproblem minimization, are not guaranteed to find an optimal solution even when unlimited time is given. However, they serve the purpose of quickly finding a good solution. Our experiments have successfully demonstrated that with the right parameters, these strategies can outperform the best incomplete solvers. In future, we would like to explore the application of approximation strategies to complete algorithms. In particular, progressively increasing the number of clusters and using approximation strategies to find good initial upper bounds that can later be exploited by complete MaxSAT algorithms.