Extended Weighted Partial MaxSAT

Chapter 3. Extending MaxSAT to Deal with Negative Weights 26

3.1 Weighted Partial MaxSAT

A weighted clause is a pair (C, w), where C is a clause and w, its weight, is a positive integer or infinity. A clause is called hard if its weight is infinity, otherwise it is soft.

A weighted partial MaxSAT (WPM) instance is a multiset of weighted clauses φ = {(C₁, w1), . . . ,(Cm, wm),(Cm+1,∞), . . . ,(C_m+m⁰,∞)}, where the firstmclauses are soft and the lastm⁰ clauses are hard. A truth assignment of φis a mapping that assigns to each variable inφ either 0 or 1.

Given a WPM instance φ and a truth assignment I, the benefit of I on φ, noted benefit(φ, I), is the sum of the weights of the soft clauses satisfied by I if I satisfies all the hard clauses, otherwise, benefit(φ, I) = −∞. φ is satisfiable if φ has a truth assignment which satisfies all the hard clauses, otherwise it is unsatisfiable. The WP-M problem for a WPWP-M instance φ is the problem of finding an optimal assignment I of φ that maximizes benefit(φ, I), that is, benefit(φ, I) ≥benefit(φ, I⁰) for an arbitrary assignmentI⁰.

Chapter 3. Extending MaxSAT to Deal with Negative Weights 27 Given an EWPM instanceφ^E and a truth assignmentI^E, thebenefit ofI^E onφ^E, noted benefit(φ^E, I^E), is the sum of the weights of the soft formulas satisfied byI^E ifI^E satis-fies all the hard formulas, otherwise,benefit(φ^E, I^E) =−∞. φ^E issatisfiable ifφ^E has a truth assignment which satisfies all the hard formulas, otherwise it isunsatisfiable. The EWPM problem for an EWPM instanceφ^E is the problem of finding an optimal assign-mentI^E ofφ^E that maximizesbenefit(φ^E, I^E), that is,benefit(φ^E, I^E)≥benefit(φ^E, I^E0) for an arbitrary assignment I^E0.

Definition 3.1. (EWPM-to-WPM Transformation).

Letφ^E = {(F₁, w1), . . . ,(Fm, wm),(Fm+1,∞), . . . ,(F_m+m⁰,∞)}be an EWPM instance wherew_i is non-zero integer and (F_i, w_i) is a soft formula (1≤i≤m). The EWPM-to-WPM transformation consists of two steps:

(1) For each soft formula (F_i, w_i), a new variableb_i is introduced. The soft formula is then transformed into a soft clause:

(i) (b_i, w_i) if w_i>0 (¬b_i,−w_i) if wi<0

and two hard formulas ensuring thatF_i and b_i are logically equivalent:

(ii) (F_i →b_i,∞) (iii) (bi→Fi,∞)

(2) Transform hard formulas into hard clauses with a satisfiability preserving CNF transformation. In this step, any satisfiability preserving CNF transformations could be applied [12].

The two hard formulas ensure that F_i and b_i are logically equivalent.

For a positive soft formula (F_i, w_i), if there is a clauseC_iwhich is satisfiability-equivalent toFi, thenbi is unnecessary. We simply transform such (Fi, wi) into (Ci, wi). Similarly for a negative soft formula (F_i, w_i), if there is a clauseC_iwhich is satisfiability-equivalent to¬F_i, we simply transform such (Fi, wi) into (Ci,−w_i).

Lemma 3.2. Let φ^E be a satisfiable EWPM instance, φ be a WPM instance obtained from φ^E by applying EWPM-to-WPM transformation, and W_neg be the sum of all neg-ative weights in φ^E.

Chapter 3. Extending MaxSAT to Deal with Negative Weights 28 If I^E is a truth assignment of φ^E and satisfies all the hard formulas in φ^E, then there exists a truth assignment I of φ such that I satisfies all the hard clauses in φ and benefit(φ^E, I^E) =benefit(φ, I) +Wneg.

Proof. We assume thatI^E satisfiespnegative soft formulas and falsifies q negative soft formulas. That is,I^E satisfies (F_i^s, w^s_i) and falsifies (F_j^f, w_j^f) wherew^s_i <0 andw_j^f <0 (1≤ i ≤p,1 ≤ j ≤ q). Then, benefit(φ^E, I^E) = W_pos^IE +Pp

i=1w_i^s where W_pos^IE denotes the sum of the weights of positive soft clauses satisfied withI^E. We should notice that Pp

i=1w^s_i +Pq

j=1w^f_j =W_neg.

Now, we make a truth assignment I of φ by extending I^E so as to satisfy all the hard clauses in φ as follows. If I^E satisfies a soft clause (F_i, w_i), we let I satisfy b_i which is a new variable introduced by the transformation, otherwise, we let I falsify bi. It is obvious that I satisfies the hard formulas (ii) and (iii) in the transformation. Thus, we can makeIsatisfy all the hard clauses inφbecause we use a satisfiability-preserving CNF transformation in (2) of the transformation. From p negative soft formulas (F_i^s, w^s_i), p soft clauses (¬b^s_i,−w^s_i) are obtained, and, from q negative soft formulas (F_j^f, w_j^f), q soft clauses (¬b^f_j,−w^f_j) are obtained by the transformation where b^s_i and b^f_j are new variables introduced. I falsifies p soft clauses (¬b^s_i,−w_i^s) and satisfies q soft clauses (¬b^f_j,−w_j^f). Thus, benefit(φ, I) = W_pos^I +Pq

j=1(−w_j^f) where W_pos^I denotes the sum of the weights of positive soft clauses satisfied with I. Here, W_pos^I = W_pos^IE because the transformation does not change the satisfiability of positive soft formulas. Therefore, benefit(φ, I) =W_pos^IE +Pq

j=1(−w^f_j).

The difference betweenbenefit(φ^E, I^E) andbenefit(φ, I) isbenefit(φ^E, I^E)−benefit(φ, I) = Pp

i=1w^s_i −Pq

j=1(−w^f_j) =Pp

i=1w^s_i+Pq

j=1w^f_j =Wneg. Consequently,benefit(φ^E, I^E) = benefit(φ, I) +W_neg.

Lemma 3.3. Let φ^E, φ, and W_neg be the same as those in Lemma 3.2. If I is a truth assignment of φ and satisfies all the hard clauses in φ, then there exists a truth assignment I^E of φ^E such that I^E satisfies all the hard formulas in φ^E and benefit(φ^E, I^E) =benefit(φ, I) +Wneg.

Proof. We make a truth assignmentI^E by restricting I to variables inφ^E. By a similar way in the proof of Lemma3.2, we conclude I^E satisfies the above conditions.

By Lemma3.2and 3.3, we conclude the following theorem.

Chapter 3. Extending MaxSAT to Deal with Negative Weights 29 Theorem 3.4. Let φ^E be a satisfiable EWPM instance and φ be a WPM instance obtained from φ^E by applying EWPM-to-WPM transformation. Then, φ is satisfiable.

Furthermore, ifI_sol^E is an EWPM solution of φ^E and I_sol is a WPM solution of φ, then benefit(φ^E, I_sol^E) = benefit(φ, I_sol) +W_neg where W_neg is the sum of all negative weights in φ^E.

Proof. According to Lemma 3.2, there exists a truth assignment I⁰ of φ such that benefit(φ^E, I_sol^E) =benefit(φ, I⁰) +W_neg. According to Lemma 3.3, there exists a truth assignmentI^0E of φ^E such thatbenefit(φ^E, I^0E) =benefit(φ, I_sol) +W_neg.

Here, benefit(φ^E, I_sol^E) ≥ benefit(φ^E, I^0E) and benefit(φ, I_sol) ≥ benefit(φ, I⁰) because benefit(φ^E, I_sol^E) and benefit(φ, I_sol) are maximal benefits. These inequalities and the above two equalities implybenefit(φ, I_sol) =benefit(φ, I⁰) andbenefit(φ^E, I_sol^E) =benefit(φ, I_sol) +W_neg.

3.2.2 Redundancy in Transformation

The hard formula (ii) for a positive soft formula and the hard formula (iii) for a negative soft formula are redundant for solving EWPM problem. That is, without these hard formulas, Theorem3.4 holds.

Proposition 3.5. Let φ^E be a satisfiable EWPM instance and φ be a WPM instance obtained fromφ^E by applying EWPM-to-WPM transformation. Letφ⁻denote a multiset of weighted clauses which are soft clauses inφ, hard clauses in φfrom hard formulas in φ^E, (ii) for negative soft formulas or (iii) for positive soft formulas. In other words,φ⁻ is obtained from φ by eliminating the hard clauses from (ii) for positive soft formulas and (iii) for negative soft formulas.

If I_sol is a WPM solution of φand I_sol⁻ is a WPM solution of φ⁻, then benefit(φ, I_sol) = benefit(φ⁻, I_sol⁻).

Proof. φ is a superset of φ⁻, and the soft clauses in φ and those in φ⁻ are the same, so Isol is a truth assignment of φ⁻ and satisfies all the hard clauses in φ⁻. Therefore, benefit(φ, I_sol)≤benefit(φ⁻, I_sol⁻) becauseI_sol⁻ gives the maximal benefit of φ⁻.

Next, we prove benefit(φ, Isol) ≥ benefit(φ⁻, I_sol⁻) by showing that I_sol⁻ satisfies all the hard clauses inφ.

Chapter 3. Extending MaxSAT to Deal with Negative Weights 30 Consider a positive soft formula (Fi, wi)(wi >0). For this soft formula, the soft clause (b_i, w_i) is generated. Assume thatI_sol⁻ falsifies the hard formula (ii) (F_i → b_i,∞), then I_sol⁻ satisfies Fi and falsifies bi. A truth assignment, that agrees to I_sol⁻ except only for the assignment to b_i, gives a benefit of φ⁻, which is w_i greater than benefit(φ⁻, I_sol⁻).

This contradicts the maximality ofbenefit(φ⁻, I_sol⁻). Consequently,I_sol⁻ has to satisfy the hard formula (ii). Thus, I_sol⁻ satisfies the hard clauses from (ii) while these clauses are not contained inφ⁻.

By the similar way, we can show that I_sol⁻ satisfies the hard clauses obtained from the hard formula (iii) for a negative soft formula. Consequently, I_sol⁻ satisfies all the hard clauses in φ.

3.2.3 Considerations

A natural interpretation of a soft formula (F, w) is that we gainwdollars whenF is true.

Under the interpretation, a negative soft formula (F,−20) means that we lose 20 dollars when F is true. (F,−20) is transformed into (¬b,20) where b is logically equivalent to F. (¬b,20) means that we gain 20 dollars whenb, i.e. F is false. Someone may consider this is strange because the original soft formula (F,−20) says nothing when F is false.

It is ordinary for us to imply that neither gain nor loss whenF is false according to the soft formula.

This strange meaning is resolved by the following settings: We pay a deposit of −w dollars for a negative soft formula (F, w)(w <0) and have−wdollars refunded when F is false.

Take (F,−20) as an example. We first pay 20 dollars as the deposit, then examine the truth value ofF. WhenF is false, we have 20 dollars refunded. Thus, the final payoff is 0 whenF is false. This is in accordance with (F,−20). WhenF is true, 20 dollars should be paid according to (F,−20). Since the deposit 20 dollars has been paid beforehand, this amount of money is taken into the consideration.

We should notice that the total deposit is−W_negdollars under the assumption of Theo-rem3.4. Thus, the expression (benefit(φ^E, I_sol^E) =benefit(φ, Isol)+Wneg ) in Theorem3.4 means that our maximal gain fromφ^E equals the difference between maximal gain from φand the total deposit.

Let us leave the interpretation and turn to MinSAT which is an alternative to MaxSAT.

MinSAT is the problem of finding a truth assignment that satisfies all the hard clauses

Chapter 3. Extending MaxSAT to Deal with Negative Weights 31 and minimizes the sum of weights of satisfied soft clause. We can say that EWPM

“minimizes” the sum of absolute values of weights of satisfied negative soft formulas.

From this point of view, we can solve MinSAT with EWPM.

Letφ^Min ={(C₁, w₁), . . . ,(C_m, w_m),(C_m+1,∞), . . . ,(C_m+m⁰,∞)}be a satisfiable weight-ed partial MinSAT instance. We make an EWPM instanceφ^Maxby negating the weights inφ^Min:

φ^Max={(C₁,−w₁), . . . ,(Cm,−w_m),(Cm+1,∞), . . . ,(C_m+m⁰,∞)}

If a truth assignment satisfies all the hard clauses inφ^Min, then it satisfies all the hard clauses inφ^Max, and vice versa. It must be noted thatbenefit(φ^{M ax}, I) =−benefit(φ^{M in}, I) where I is a truth assignment. This implies that benefit(φ^{M ax}, I) becomes larger as benefit(φ^{M in}, I) becomes smaller. Consequently, a MinSAT solution ofφ^Min, which gives the minimum benefit ofφ^Min, is a MaxSAT solution ofφ^Max, which gives the maximum benefit of φ^Max. Reversely, a MaxSAT solution of φ^Max is a MinSAT solution of φ^Min. In short,φ^Min andφ^Maxhave the same solution; accordingly, we may say that EWPM is not only an extension of MaxSAT but also that of MinSAT, or EWPM is an integration of MaxSAT and MinSAT.