Resolution in Max-SAT and its relation to local consistency in weighted CSPs

1 Introduction

Since the eighties, both boolean satisfiability and constraint satisfaction have been the topic of intense algorithmic research. In both areas, the goal is to assign values to variables in such a way that no forbidden combination of values appear in the solution. In satisfiability, forbidden combinations are specified by means of clauses. In constraint satisfaction they are specified by means of arbitrary constraints. Given its similarity, it is hardly a surprise that both research communities have developed closely related techniques.

In both fields, the original decision problem (SAT and CSP, respectively) has been augmented to deal with unfeasible problems (namely, not all the clauses or constraints can be satisfied). The new goal is to find an assignment that best respects the clauses/constraints. Two well-known examples are Max-SAT [Hansen and Jaumard, 1990] and weighted CSP (WCSP) [Bistarelli et al., 1999], where most of recent algorithmic work has focused. In both cases the importance of the clauses/constraints is given by a weight and the goal is to minimize the sum of weights associated with the clauses/constraints violated by the assignment. It is known that Max-SAT instances can be translated into WCSP instances and vice versa [de Givry et al., 2003]. In both cases the main solving technique are enumeration algorithms based on branch and bound search.

In the CSP side, several local consistency properties have been recently generalized to the WCSP framework [Cooper, 2003; Larrosa and Schiex, 2004; 2003; de Givry et al., 2005]. As a result, a new family of algorithms have been proposed. Besides being efficient, these algorithms have a highly desirable property: they can be neatly described as a basic backtracking search in which certain local consistency property is enforced at every search state.

In [de Givry et al., 2003], it was shown that Max-SAT instances could be efficiently solved by translating them into equivalent WCSP instances and later using a WCSP solver. The level of local consistency maintained by the WCSP solver was fundamental in the efficiency of the algorithm.

In this paper we analyze the interpretation of WCSP local consistency properties and related algorithms when applied to Max-SAT instances. To facilitate the connection, we start by providing a reformulation of Max-SAT in which it is possible to explicitly express a lower and an upper bound of the optimal cost (Section 3). Such reformulation makes possible an elegant extension of DPLL in which each branching point is just a Max-SAT instance, similarly to what happens with DPLL in SAT (Section 4). In Section 5 we present our main contribution: a generalization of the resolution rule (x∨A, ¯ x∨B⇒A∨B) and the proof that neighborhood resolution (i.e., a restricted form of resolution) suffices to enforce (weighted) node and arc consistency. In Section 6 we put our approach in context with other Max-SAT algorithms. Finally, in Section 7 we provide conclusions and directions of future work.

2 Preliminaries

In the sequel X = {x1, . . . ,xn} will denote a set of boolean variables. They take values over the set {t, f}, which stands for true and false, respectively. A literal l is either a variable x or its negation ¯ x. ¯ l stands for the negation of l.

If variable x is instantiated to t, noted x←t literal x is satisfied and literal ¯ x is falsified. Similarly, if x is instantiated to f, ¯ x is satisfied and x is falsified. An assignment is an instantiation of a subset of the variables. The assignment is complete if it instantiates all the variables in X (otherwise it is partial). An assignment satisfies a clause (i.e., a disjunction of literals) C iff it satisfies one or more of its literals. It satisfies a set of clauses F iff it satisfies all its clauses. A satisfying complete assignment is called a model. Given a boolean formula encoded by a set of clauses F , the SAT problem consists in determining whether there is any model for it or not.

We will use the symbol ✷ to denote the empty clause which, obviously, cannot be satisfied. When ✷ ∈ F we say that there is an explicit contradiction.

When there is no model for the formula F , one may be interested in finding the complete assignment with minimum number of violated clauses. This problem is known as MaxSAT.

3 An equivalent reformulation of Max-SAT

There is a weighted version of Max-SAT in which (weighted) clauses are pairs (C,w) such that C is a classical clause and w is the cost of its falsification. In weighted Max-SAT F is a set of weighted clauses. The cost of an assignment is the sum of weights of all the clauses that it falsifies. The goal is to find complete assignments with minimal cost. We make the usual assumption of weights being natural numbers.

It is easy to see that Max-SAT and weighted Max-SAT have exactly the same expressive power. A Max-SAT instance can be rewritten as a weighted instance replacing every clause C by a weighted clause (C,1). A weighted MaxSAT instance can be rewritten as a Max-SAT instance replacing every weighted clause (C,w) by w copies of clause C. Clearly, weighted Max-SAT encodings may be exponentially more compact than Max-SAT. Thus, in the following, we will assume, without loss of generality, weighted Max-SAT.

Following previous work in weighted constraint satisfaction [Larrosa and Schiex, 2004], we assume the existence of a known upper bound k of the optimal solution. This is also done without loss of generality because, if a tight upper bound is not known, k can be set to the sum of weights of all the clauses.

Consider the set F of weighed clauses. We say that a model is a complete assignment with cost less than k. MaxSAT is the problem of finding a model of minimal cost, if there is any.

Observe that weights w ≥ k indicate that the associated clause must be necessarily satisfied. Thus, we can replace every weight w ≥ k by k without changing the problem. Thus, without loss of generality we assume all costs in the interval [0..k] and, accordingly, redefine the sum of costs as

in order to keep the result within the interval. For convenience of notation, we will refer to k as ⊤. We say that a weighted clause is hard (or mandatory) iff its weight is ⊤. Observe that Max-SAT with ⊤ = 1 is equivalent to SAT.

Example 1 Consider the formula {(x,1),(¯ y, 5), ( ¯ x ∨ y,2),(x∨y,4)}, with ⊤= 5. The second clause is hard. The assignment x = f,y = f is not a model because its cost is 1⊕4 =⊤. The assignment x←t,y←f is a (optimal) model with cost 2.

Note that in Max-SAT truth tables are tables with a cost associated to each truth assignments. A brute-force solving method consists in computing the truth table of the input formula and finding the minimal cost model. For instance, the truth-table of the previous formula is,

It is worth mentioning the role of the empty clause (✷,w). Since it cannot be satisfied, w will be added to the cost of any model. Therefore, w is an explicit lower bound of the optimal model. When the lower bound and the upper bound have the same value (i.e., (✷,⊤) ∈ F ) the formula does not have any model and we call this situation an explicit contradiction.

4 Generalization of DPLL toMax-SAT

4.1 Max-SAT Basic Simplification Rules

SAT solvers take advantage from some equivalence rules that are used to simplify the CNF formula without changing its set of models. Not all of these formulas can be applied directly to Max-SAT. In this Section we state some useful Max-SAT specific rules. We use the notation [P, . . . ,Q] ⇒ [R, . . . , S], where P,Q, . . . are weighted clauses. It means that if there are in F weighted clauses matching with [P, . . . ,Q], they can be replaced by [R, . . . ,S]. A and B are arbitrary disjunctions of literals.

• BR1: [(A,⊤),(A∨B,w)]⇒[(A,⊤)]
• BR2: [(A,w),(A,u)]⇒[(A,w⊕u)]
• BR3: If (w ⊕ u = ⊤) then [(A,w),(A ∨ B,u)] ⇒ [(A, w), (A ∨ B, ⊤)]
• BR4: [(A,0)]⇒[ ]

BR1 shows that classical absorption can only be applied when the absorbing clause is hard. BR2 generalizes the standard idempotency of the conjunction: In Max-SAT the weights of the repeated clauses must be added in the resulting clause. BR3 is used to harden a soft clause. BR4 indicates that cost-free clause can be eliminated. The correctness of these equivalences is direct and we omit the proof.

Example 2 Consider the formula {(x,1),(x,1),(x ∨ y,3),(x∨y∨z,1)}, with ⊤ = 5. We can apply BR2, which produces {(x,2),(x∨y,3),(x∨y∨z,1)}. Now, we can apply BR3, producing {(x, 2), (x∨y,⊤), (x∨y∨z, 1)}. Finally, BR1 produces {(x,2),(x ∨ y,⊤)}. The equivalence between the original and the final formula can be checked by constructing and comparing the costs of the two truth-tables.

4.2 Max-DPLL

Davis Putnam (DPLL) is the most popular algorithm for SAT and the starting point of most state-of-the-art solvers [Davis et al., 1962]. It takes as input a CNF formula F and decides whether or not there exists a model. In this Section, we present a natural extension of DPLL to Max-SAT that we call Max-DPLL. Let F be a weighted CNF formula and ⊤ its upper bound. Max-DPLL(F ,⊤) returns the cost of the optimal model of F if there is such a model, else it returns ⊤. The following description is inspired by the description of DPLL given in [Bacchus, 2002].

As in classical SAT, Max-DPLL performs basic simplifications on its input prior to invoking itself recursively. The instantiation of a variable by forcing the satisfaction of a literal l, denoted F [l] produces a new formula generated from F as follows: all clauses containing l are eliminated, and ¯ l is removed from all clauses where it appears. Unit Clause Reduction (UCR) is another simplification rule that selects a clause (l,⊤) (namely, a unit hard clause) and instantiates the corresponding variable in accordance to the literal in that clause. Unit Propagation (UP) is the algorithm that performs UCR and the basic simplification rules BR1-4 until either (a) a contradiction is achieved, or (b) there are no more possible simplifications to do.

Example 3 Consider the application of UP to the formula {(✷,1),(¯ x, 4), (x, 1), (y, 3), ( ¯ y, 1), ( ¯ x ∨ ¯ y ∨ z,1)}, with ⊤ = 5. Rule BR3 transforms it into {(✷, 1), ( ¯ x, ⊤), (x, 1), (y, 3), ( ¯ y, 1), ( ¯ x ∨ ¯ y ∨ z,1)}. UCR instantiates ¯ x and produces {(✷,3),(y,3),(¯ y, 1), ( ¯ y ∨ z, 1)}. Again BR3 produces {(✷,3),(y,⊤),(¯ y, 1), ( ¯ y∨z,1)}, which allows UCR to instantiate y, {(✷,4),(z,1)}. Again BR3 produces {(✷,4),(z,⊤)}, which UCR to instantiate z producing the trivial {(✷,4)}. The model of the original formula ( ¯ x, y, z) can be constructed by tracking back the truth assignments made by UCR.

A recursive description of Max-DPLL is given in Algorithm 1. First, UP is applied to the input formula (line 1). If the resulting formula contains a contradiction, the algorithm returns ⊤ and backtracks (line 2). Else, if it does not contain any variable the trivial cost of the optimal model is returned (lines 3 and 4). Otherwise, an arbitrary literal l is selected (line 5). The formula is instantiated with l and ¯ l and MaxDPLL is recursively called with each case (lines 6 and 7). Observe that the first recursive call is made with the ⊤ inherited from its parent, but the second call uses the output of the first call. This implements the typical upper bound updating of branch and bound. Finally, the best value of the two recursive calls is returned (line 8). Note that if Max-DPLL is executed with a SAT instance (i.e., ⊤ = 1) it behaves exactly as DPLL.

Figure 1 reports some empirical evaluation of Max-DPLL on 40-variable random instances of Max-2-SAT and Max-3SAT generated with the Cnfgen generator. 1 The horizontal axis indicates the number of clauses and the vertical axis indicates the search effort as the number of visited nodes. Each

1 A. van Gelder ftp://dimacs.rutgers.edu/ pub/challenge/satisfiability/contributed/UCSC/instances

Function Max-DPLL(F ,⊤) : nat 1 F :=UP(F ); 2 if (✷,⊤) ∈ F then return ⊤; 3 if F = /0 then return 0; 4 if F = {(✷,w)} then return w; 5 l :=SelectLit(F ); 6 v :=Max-DPLL(F [ l ],⊤); 7 v :=Max-DPLL(F [ ¯ l ],v); 8 return v;

Algorithm 1: Max-DPLL. F is a set of weighted clauses with all weights in the interval [0, . . . ,⊤]. If the weighted formula has models, Max-DPLL returns the cost of the optimal one, else it returns ⊤

point is the mean over 10 instances. The results of MaxDPLL are those labelled as UP (ignore, for the moment, the other curves). As can be observe, the performance of the algorithm degenerates as the number of clauses increases.

Max-DPLL can be enhanced by dominance rules that exploit situations where it is easy to detect that one literal is never worse than its negation. A well-known SAT case, also applicable to Max-SAT, is the pure literal rule. It says that if there is a literal such that it appears in the formula and its negation does not appear, then all clauses mentioning it can be removed. More sophisticated dominance rules for MaxSAT and WCSP can be found in [Xing and Zhang, 2004; de Givry, 2004].

5 Resolution for Max-SAT

While DPLL seems to be the best option to find models, resolution might be more appropriate to detect contradictions. [Robinson, 1965] showed that the resolution rule is sound and complete for SAT, although it is usually too space consuming. In the SAT context, the performance of DPLL has been improved by the addition of limited forms of resolution at each search node [Gelder, 1995; Rish and Dechter, 2000; Bacchus, 2002; Drake et al., 2002] in order to anticipate the detection of dead-ends. In this section we generalize the resolution rule to Max-SAT. Then we show that some local consistency techniques used in [Larrosa and Schiex, 2004] are just the application of a restricted form of the weighted resolution rule.

First we define the subtraction of weights (⊖): Let a,b ∈ [0, . . . ,⊤] be two weights such that a ≥ b,

The weighted resolution rule (RES) is defined as,

where A and B are arbitrary disjunctions of literals and m = min{u,w}. Variable x is called the clashing variable. Observe that in the u = w = ⊤ case the fourth and fifth new n. of clauses clauses can be removed (by BR1), yielding a rule similar to classical resolution. Observe as well that in the u = w <⊤ case, the second and third new clauses will have weight 0 and can be removed (by BR4). In the u ̸=w case, either the second or the third new clause will have weight 0 and can be removed (by BR4). Recall that in RES, the left-hand clauses are replaced by the right-hand, while in classical resolution right-hand clauses are just added.

Figure 1: Experimental results on random Max-2SAT (top) and Max-3SAT (bottom).

Theorem 1 The transformation rule RES is sound. Namely, it preserves the set of models and their cost.

proof 1 The following table contains in the first columns all the truth assignments, in the second column the cost of the assignment according to the clauses on the left-hand of the RES rule, and in the third column the cost of the assignment according to the clauses on the right-hand of the RES rule. As it can be observed, the costs the are same, so the resulting problem is equivalent.

The interest of RES is that it makes explicit some previously hidden connection between variables in A and B. It is well known that in the SAT case (i.e, ⊤= 1) the rule is complete (its application suffices to achieve a contradiction). We are still investigating under which other cases the completeness of RES is guaranteed. One important problem we have detected is that the fourth and fifth new weighted formulas (i.e., (x∨A∨ ¯ B,m), (¯ x∨ ¯ A∨B,m)) may not be in conjunctive normal form.

5.1 Neighborhood Resolution

Neighborhood Resolution [Cha and Iwama, 1996] is the classical resolution rule restricted to pairs of clauses that differ only in the clashing variable. Similarly, in the Max-SAT context we define the neighborhood resolution rule (NRES) as RES restricted to the A = B case, which simplifies to,

whith m =min{u,w}. This rule is specially useful because it projects to A costs that were implicit in the formula. We demonstrate the interest of NRES considering its application to bounded-size clauses. Let NRESk denote NRES restricted to |A| = k. NRES0 yields,

This rule is extremely useful because it produces a direct increment of the lower bound, which may raise a contradiction, or produce new unit clause reductions.

Example 4 Consider the formula {(x, 1), ( ¯ x, 2), (y, 1), ( ¯ y,1),(z,1)} with ⊤ = 3. UP is unable to simplify the problem. Nevertheless, NRES0 can be applied to the first and second clauses producing {(✷, 1), ( ¯ x, 1), (y, 1), ( ¯ y,1),(z,1)}. Appling NRES0 to the third and fourth clauses produces {(✷,2),(¯ x, 1), (z, 1)}. Using BR3 we obtain {(✷,2),(¯ x,⊤),(z,⊤)}. The two unit clauses can be reduced, producing {(✷,2)}.

It is interesting to observe that the application of NRES0 is somehow similar to the computation of the lower bound of [Alsinet et al., 2003]. The practical importance of adding NRES0 to Max-DPLL is illustrated in Figure 1. The lines labelled UP+NRES0 report the efficiency of Max-DPLL when UP is augmented with NRES0 until quiescence. As it can be observed NRES0 produces huge savings over the very inefficient Max-DPLL.

The rule NRES1 is,

This rule is also of great interest because it increases the weight of a unary clauses, which may allow further application NRES0 and UCR.

Example 5 Consider the formula {(x ∨ y,1),(¯ x ∨ y, 1), ( ¯ y,1),(z,1) with ⊤ = 2. Neither UP nor NRES0 can simplify the problem. However, NRES1 produces

{( ¯ y,1),(y,1),(z,1)} which allows NRES0 to transform the problem into {(✷,1),(z,1)}. We can apply BR3 to the unary clause obtaining {(✷,1),(z,⊤). Now, UCR produces {(✷, 1)}.

The practical importance of adding NRES1 to MaxDPLL is also illustrated in Figure 1. The lines labelled UP+NRES0+NRES1 report the efficiency of Max-DPLL when UP is augmented with NRES0 and NRES1 until quiescence. As it can be observed, the addition of NRES1 also produces huge gains. For the sake of completeness, we also evaluate the effect of NRESk for k > 1. Obviously, in 2-SAT it does not have any effect, since the application of NRESk requires clauses of length k+1. In 3-SAT, NRES2 can only be applied in the original ternary clauses. Its effect is reported in Figure 1 under the label UP+NRES. It can be observed that NRES2 has a very limited effect.

5.2 Neighborhood Resolution and Local Consistency

In this Section we relate the simplification rules discussed along the paper with local consistency properties developed for WCSP. In order to do so, we recall that the usual way to map a Max-SAT instance with a WCSP is to group clauses mentioning exactly the same set of variables and associate them to a cost function f defined as follows: Let V ⊂ F be the group of clauses over the set of variables Y ⊂ X. V defines a cost function f with scope Y. Let t be an instantiation of the variables in Y. If t falsifies a clause (C,w) ∈V , f (t) =w, else f (t) = 0. Now it is straightforward to redefine the WCSP local consistency properties in Max-SAT terms. In the following consider a boolean formula F where w(✷) denotes the weight of the empty clause; w(i) and w(¯ i) the weights of the the unary clauses xi and ¯ xi, respectively; analogously w(i j), w(i ¯ j), w(¯ i j) and w(i j) are the weights of the four possible binary clauses over xi and xj. If any of these clauses is not in F the corresponding weight is 0.

Definition 1 F is node-consistent (NC) iff for all variable xi, w(✷) ⊕ w(i) < ⊤ and w(✷) ⊕ w(¯ i) < ⊤.

Theorem 2 Algorithm UP enforces the NC property.

proof 2 Suppose that F is not NC. Then there is some clause (l,w) ∈ F such that w(✷)⊕w =⊤. Therefore BR3 can be applied replacing clause (l,w) by (l,⊤). It will allow the application of UCR which will eliminate the clause.

Definition 2 F is star node-consistent (NC*) iff it is NC and for all variable xi, w(i) = 0 or w(¯ i) = 0

Theorem 3 Let UP +NRES0 denote the algorithm that applies UP and NRES0 until quiescence. It enforces NC*.

proof 3 We only need to proof that the application of NRES0 guarantees that for all variable xi, w(i) = 0 or w(¯ i) = 0. Assume that 0 < w(i) ≤ w(¯ i). There are two possible situations. The first one is w(¯ i) = ⊤. In that case UP will trigger UCR and xi will disappear from the formula. The second situation is w(¯ i) < ⊤. Then, the application of NRES0 will add w(i) to w(✷) and replace (xi,w(i)),( ¯ xi , w(¯ i)) by (xi , 0), ( ¯ xi , w(¯ i) ⊖ w(i)).

The algorithm to enforce NC* introduced in [Larrosa and Schiex, 2004] proves the following result,

Corollary 1 UP +NRES0 can be implemented with time complexity O(n), where n is the number of variables in the formula.

Definition 3 F is arc-consistent (AC*) iff it is NC* and for all pair of variables (xi,xj), min{w(i j),w(i ¯ j)} = 0 and min{w(¯ i j),w(i j)} = 0

Theorem 4 Let UP +NRES0 +NRES1 denote the algorithm that applies UP, NRES0 and NRES1 until quiescence. It enforces arc-consistency (AC*).

proof 4 We only need to proof that the application of NRES1 guarantees that for all pair of variables (xi,xj), min{w(i j),w(i ¯ j)} = 0 and min{w(¯ i j),w(i j)} = 0. We proof the first condition (the second is similar). Assume that 0 < w(i j) ≤ w(i ¯ j). There are two possible situations. The first one is that w(i j) =⊤ (which implies w(i ¯ j) =⊤. In that case NRES1 will add (xi,⊤) to the formula. Then, UCR will be trigger and xi will disappear from the formula. The second situation is w(i j) <⊤. Then, the application of NRES1 will add w(i j) to w(i) and replace (xi ∨x j,w(i j)), (xi ∨ ¯ x j , w(i ¯ j)) by (xi ∨ x j , 0), (xi ∨ ¯ x j , w(i ¯ j)⊖w(i j)).

The algorithm to enforce AC* introduced in [Larrosa and Schiex, 2004] proofs the following result.

Corollary 2 UP +NRES0 +NREO can be implemented with time complexity O(n 2 ), where n is the number of variables in the formula.

6 Neighborhood Resolution and state-of-the-art Max-SAT lower bounds

In the last years several algorithms for Max-SAT have been proposed [Alsinet et al., 2003; Xing and Zhang, 2004; Shen and Zhang, 2004]. All these works have in common a basic branch and bound algorithm. They mainly differ in the lower bound that they use. [Shen and Zhang, 2004] show that their lower bound is better (i.e., higher than or equal) than [Alsinet et al., 2003] and, under some reasonable conditions, it is also better than [Xing and Zhang, 2004]. In the following, by means of two examples, we show that UP +NRES0 +NRES1 is not comparable with them.

Consider the formula {(x ∨ z,1),(¯ x ∨ z, 1), (y ∨ ¯ z, 1), ( ¯ y ∨ ¯ z,1)}. Both [Xing and Zhang, 2004] and [Shen and Zhang, 2004] would compute a lower bound 0. However, NRES1 can be applied twice, producing the equivalent formula {(z, 1), (¯ z, 1)} and now NRES0 would transform the problem into {(✷, 1)}, which means a lower bound of 1.

Consider now the formula {(x,1),(y,1),(¯ x∨ ¯ y,1)}. While both [Xing and Zhang, 2004] and [Shen and Zhang, 2004] would compute a lower bound of 1, NRES cannot be applied, so the implicit lower bound of our algorithm would be 0. Nevertheless, it is important to observe that, if we encode this problem as a weighted CSP and enforce a stronger form of consistency called existential directional arc consistency (EDAC*)[de Givry et al., 2005], we transform the formula into the equivalent {(✷,1),(x ∨y,1)} which also has an implicit lower bound of 1. The performance of enforcing EDAC* on random Max-SAT instances is also illustrated in Figure 1. As it can be seen, it clearly provides further improvement over the application of the NRES rule. Experiments on Max-SAT using weighted CSP technology can be performed using the freely available toolbar solver. 2

7 Conclusions and Future work

Motivated by the success of [de Givry et al., 2003] in solving Max-SAT instances as weighted CSPs, we have studied the interpretation of WCSP local consistency properties within the Max-SAT context. The result of our work is a logical framework for Max-SAT in which the solving process can be seen as a set of transformation rules. Interestingly, our approach leads to a natural extension of the Davis-Putnam algorithm as well as an extension of the resolution rule (RES). The application of a limited form of RES, called neighborhood resolution (NRES), provides an interesting and effective algorithm. We have shown the relation between the application of NRES and some local consistency properties in weighted CSP. Finally, we have also shown that NRES provides (implicit) lower bounds not subsumed by state-of-the-art MaxSAT solvers.

We believe our work leaves several directions of future work. First, it would be interesting to analyze under which conditions the application of RES provides a complete method for Max-SAT. Since it has been shown that directional resolution is just an instantiation of adaptive consistency [Rish and Dechter, 2000], it would also be interesting to know if there is any relation between the application of RES and the more general bucket elimination [Dechter, 1999].

Our framework facilitates the relation between Max-SAT and weighted CSP solving. The resolution rule that we have introduced seems only valid to enforce node and arc consistency. However, it is known in the WCSP context that stronger forms of local consistency such as EDAC* may be more effective in practice [de Givry et al., 2005]. Thus, it seems natural to search for new transformation rules such that, when added to NRES, can achieve higher levels of local consistency.