The Logic Behind Weighted CSP

1 Introduction

The Weighted Constraint Satisfaction Problem (WCSP) is a well known soft constraint framework for modelling overconstrained problems with practical applications in domains such as resource allocation, combinatorial auctions and bioinformatics. WCSP is an optimization version of the CSP framework in which constraints are extended by associating costs to tuples. Solving a WCSP instance, which is NP-hard, consists in finding a complete assignment of minimal cost.

Global consistency WCSP algorithms such as Bucket Elimination [Dechter, 1999] solve WCSP instances without search. They obtain an optimal solution by applying, to the original instance, transformations that preserve cost distributions. On the other hand, WCSP Branch and Bound (BnB) based algorithms such as PFC [Freuder and Wallace, 1992], PFC-MRDAC [Larrosa and Meseguer, 1996], Russian Doll Search [Verfaillie et al., 1996], MAC∗ [Larrosa and Schiex, 2004], MFDAC∗ [Larrosa and Schiex, 2003] and MEDAC∗ [de Givry et al., 2005] perform a systematic search in the space of all possible assignments. They differ in the method of computing a lower bound at each node of the proof tree to prune some parts of the search space. Modern algorithms such as MAC∗ , MFDAC∗ and MEDAC∗ enforce some extension of Arc Consistency (AC) to WCSP -Soft AC (AC∗ ), Full Directional AC (FDAC∗ ) or Existential Directional AC (EDAC∗)-when computing that lower bound.

In this paper we relate ideas from three different research communities -Multiple-Valued Logic, Satisfiability and Constraint Processing- with the aim of describing the Jordi Levy and FelipMany`a IIIA, CSIC

∗This research was founded by the MEC research projects iDEAS (TIN2004-04343), Mulog (TIN2004-07933-C03-01/03) and SofSAT (TIC2003-00950), and the program Ram´on y Cajal.

Campus UAB, Bellaterra, Spain

underlying logic of WCSP. First, we define an encoding, called signed encoding, that transforms any WCSP instance to a Signed Max-SAT instance, where Signed Max-SAT is the Max-SAT problem of the multiple-valued clausal forms known as Signed CNF formulas (see [Ans´otegui and Many`a, 2003] and references therein). Second, we define a complete resolution calculus for solving Signed Max-SAT. Third, we devise an exact algorithm for solving WCSP from the completeness proof of the resolution calculus. Fourth, we define several sound inference rules for Signed Max-SAT that enforce some known arc consistency properties when applied to the signed encoding of any binary WCSP instance.

The structure of the paper is as follows. Section 2 contains preliminary definitions and the signed encoding. Section 3 defines the inference rule for signed Max-SAT and proves its soundness and completeness. Section 4 describes an exact algorithm for solving Weighted CSP. Section 5 defines four derived rules that enforce soft local consistency properties. Finally, Section 6 presents the conclusions of our work.

2 Preliminaries

Definition 1 A truth value set, or domain, N is a non-empty finite set {i1, i2, . . . , in} where n denotes its cardinality. A sign is a subset S ⊆ N of truth values. A signed literal is an expression of the form S:p, where S is a sign and p is a propositional variable. The complement of a signed literal l of the form S:p, denoted by l, is S:p = (N \ S):p. A signed clause is a disjunction of signed literals. A signed CNF formula is a multiset of signed clauses.

Definition 2 An assignment for a signed CNF formula is a mapping that assigns to every propositional variable an element of the truth value set. An assignment I satisfies a signed literal S:p iff I(p) ∈ S, satisfies a signed clause C iff it satisfies at least one of the signed literals in C, and satisfies a signed CNF formula Γ iff it satisfies all clauses in Γ. A signed CNF formula is satisfiable iff it is satisfied by at least one assignment; otherwise it is unsatisfiable.

Definition 3 The Signed Max-SAT problem for a signed CNF formula consists in finding an assignment that minimizes the number of falsified signed clauses.

Definition 4 A constraint satisfaction problem (CSP) instance is defined as a triple 〈X,D,C〉, where X =

{x1, . . . , xn} is a set of variables, D = {d(x1), . . . , d(xn)} is a set of domains containing the values the variables may take, and C = {C1, . . . ,Cm} is a set of constraints. Each constraint Ci = 〈Si,Ri〉 is defined as a relation Ri over a subset of variables Si = {xi1 , . . . , xik }, called the constraint scope. The relation Ri may be represented extensionally as a subset of the Cartesian product d(xi1 ) × · · · × d(xik ).

Definition 5 An assignment v for a CSP instance 〈X,D, C〉 is a mapping that assigns to every variable xi ∈ X an element v(xi) ∈ d(xi). An assignment v satisfies a constraint 〈{xi1 , . . . , xik }, Ri〉 ∈ C iff 〈v(xi1 ), . . . , v(xik )〉 ∈ Ri.

Definition 6 A Weighted CSP (WCSP) instance is defined as a triple 〈X,D,C〉, where X and D are variables and domains as in CSP. A constraint Ci is now defined as a pair 〈Si, fi〉, where Si = {xi1 , . . . , xik } is the constraint scope and fi : d(xi1 ) × · · · × d(xik ) → N is a cost function. The cost of a constraint Ci induced by an assignment v in which the variables of Si = {xi1 , . . . , xik } take values bi1 , . . . , bik is fi(bi1 , . . . , bik ). An optimal solution to a WCSP instance is a complete assignment in which the sum of the costs of the constraints is minimal.

Definition 7 The Weighted Constraint Satisfaction Problem (WCSP) for a WCSP instance consists in finding an optimal solution for that instance.

Definition 8 The signed encoding of a WCSP instance 〈X,D,C〉 is the signed CNF formula over the domain N = ⋃xi∈D d(xi) that contains for every possible tuple 〈bi1 , . . . , bik 〉 ∈ d(xi1 ) × . . . × d(xik ) of every constraint 〈{xi1 , . . . , xik }, fi〉 ∈ C, fi(bi1 , . . . , bik ) copies of the signed clause:

An alternative encoding is to consider signed clauses with weights instead of allowing multiple copies of a clause. For the sake of clarity we use unweighted clauses. Nevertheless, any efficient implementation of the algorithms proposed should deal with weighted clauses. The extension of our theoretical results to weighted clauses is straightforward.

Proposition 9 Solving a WCSP instance P is equivalent to solving the Signed Max-SAT problem of its signed encoding; i.e., the optimal cost of P coincides with the minimal number of unsatisfied signed clauses of the signed encoding of P .

PROOF: For every combination of values to the variables of the scope of a constraint Ci = 〈Si, fi〉 , the signed encoding contains as many clauses as the cost associated with that combination. If an assignment of the signed encoding restricted to the variables of Si coincides with a combination of Ci with cost 0, then all the clauses of the signed encoding introduced by Ci are satisfied because there is no clause forbidding that combination. If an assignment of the signed encoding restricted to the variables of Si coincides with a combination 〈bi1 , . . . , bik 〉 of Ci with cost u, where u > 0, then, by construction of the signed encoding, only the u clauses of the form {bi1 }:xi1 ∨ · · · ∨ {bik }:xik are falsified among the clauses introduced by Ci.

Example 10 Figure 1 shows a WCSP instance 〈X,D,C〉 and its signed encoding. The WCSP has the set of variables X = {x1, x2, x3} with domains d(x1) = d(x2) = d(x3) = {a, b, c}. There is a binary constraint between variables x1 and x2, a binary constraint between variables x2 and x3, and a unary constraint for every variable. Unary costs are depicted inside small circles. Binary costs are depicted as labeled edges connecting the corresponding pair of values. The label of each edge is the corresponding cost. If two values are not connected, the binary cost between them is 0. In this instance, the optimal cost is 2.

3 The Inference Rule. Soundness and Completeness

We define a resolution rule for solving signed Max-SAT, called Signed Max-SAT Resolution, and prove its soundness and completeness. This rule was inspired by previous works [Larrosa and Heras, 2005; Bonet et al., 2006] for Max-SAT. The completeness proof for signed CNF formulas is technically more involved than the proof for Boolean CNF formulas.

Definition 11 The Signed Max-SAT Resolution rule is defined as follows

This inference rule is applied to multisets of clauses, and replaces the premises of the rule by its conclusions. We say that the rule resolves the variable x.

The tautologies concluded by the rule like N:x ∨ A are removed from the resulting multiset. Also we substitute clauses like S :x∨S ′ :x∨A by (S ∪ S ′ ):x∨A, and clauses like ∅:x∨A by A.

We would like to emphasize that the rule does not add the conclusions to the premises. It replaces the clauses in the premises by the clauses in the conclusions.

Definition 12 We write C ⊢ D when the multiset of clauses D can be obtained from the multiset C applying the rule finitely many times. We write C ⊢x C′ when this sequence of applications only resolves the variable x.

In the context of Max-SAT problems, an inference rule is sound iff the number of falsified clauses in the premises is equal to the number of falsified clauses in the conclusions for any assignment.

Theorem 13 (Soundness) The signed Max-SAT resolution rule is sound.

PROOF: Let I be an arbitrary assignment. There are four cases:

1. If I falsifies the two premises, then I also falsifies the first two conclusions, and only them.

2. If I satisfies the two premises, then it also trivially satisfies the last s+t clauses of the conclusion, because they are either implied by one or the other premise. The second clause of the conclusion is implied by each one of the premises. Therefore, it is also satisfied by I.

The first clause of the conclusion is not implied by the premises. However, if both premises are satisfied then we have two cases. If S:x and S ′ :x are both satisfied, then so it is (S ∩ S ′ ):x. Otherwise, either some ai's or some bj's is satisfied, thus also the first clause of the conclusion.

3. If I satisfies the first premise, but not the second one, then the second clause of the conclusion as well as the t following clauses are satisfied, because all them are implied by the first premise.

For the rest of conclusions, there are two cases: If some of the ai's is satisfied, then let i be the index of such a. The assignment will satisfy the first clause of the conclusion and the last s conclusions, except S ′ :x ∨ b1 ∨ . . . ∨ bt ∨ a1 ∨ . . . ∨ ai-1 ∨ ai that is falsified. Otherwise none of the ai's is satisfied, and therefore, S:x is satisfied. Hence, the first conclusion is falsified, and the last s conclusions are satisfied. 4. If I satisfies the second premise, but not the first one, the situation is analogous to previous case.

Definition 14 A multiset of clauses C is said to be saturated w.r.t. x if, for every pair of clauses C1 = S:x ∨ A and C2 = S ′ :x ∨ B of C,

i) there are literals S1:y in A and S2:y in B such that S1 ∪ S2 = N, or

A multiset of clauses C ′ is a saturation of C w.r.t. x if C ′ is saturated w.r.t. x and C ⊢x C ′ , i.e. C ′ can be obtained from C applying the inference rule resolving x finitely many times.

We assign to every clause C a score s(C) equal to the number of assignments to the variables that falsify C. The score of a multiset of clauses is the sum of scores of the clauses contained in it.

Lemma 15 For every multiset of clauses C and variable x, there exists a multiset C ′ such that C ′ is a saturation of C w.r.t. x.

PROOF: We proceed by applying nondeterministically the inference rule resolving x, until we obtain a saturated multiset. We only need to prove that this process terminates in finitely many inference steps, i.e that there does not exist infinite sequences C = C0 ⊢ C1 ⊢ . . ., where at every inference we resolve the variable x and none of the sets Ci are saturated. Let M be the score of C.

Let us partition the multiset C of clauses into n multisets (n is the size of the domain), {B0, B1, . . . , Bn-1}, where Bi contains the clauses where the cardinality of the support of x is i. Notice that B0 is the multiset of clauses that do not contain the variable x. Let us denote by s(Bi) the score of the multiset Bi.

We will look at this n multisets as a word of length n and base M+1. So our multiset will be represented by the number s(B0) s(B1) · · · s(Bn-1), taking s(B0) as the most significant digit. Since Bi is a subset of C, for i = 0, . . . , n - 1, s(Bi) ≤ M.

When we apply our inference rule, we take two clauses, say one from Bi and one from Bj and substitute them by a set of clauses that we will distribute among the different Bk's. Now we have a new multiset of clauses and by the soundness of our rule the score of the new multiset is the same. But, if we again look at the multiset as a number in base M, the number will be different. We will argue that for each inference step, the number increases. Say that the clauses we do inference are S:x ∨ A ∈ B|S| and S ′ :x ∨ B ∈ B|S′ |. By the inference step we remove these clauses and add some clause in B|S∩S′ |, and maybe also some clauses in B|S|, B|S′ | and B|S∪S′ |. Since, by definition of saturation S ∩ S ′ ̸= S and S ∩ S ′ ̸= S ′ , we know that |S ∩ S ′ | < |S|, |S ′ | < |S ∪ S ′ |, hence the digit of B|S∩S′ | is more significant than the digits of B|S|, B|S′ | and B|S∪S′ |. We have to conclude that the newM-base number after the inference step is larger than before. Since the largest possible number we can obtain is the one represented as s(B0)s(B1) · · · s(Bn-1) = M0 · · · 0 the saturation procedure for x has to finish before M n steps.

Lemma 16 Let E be a saturated multiset of clauses w.r.t. x. Let E ′ be the subset of clauses of E not containing x. Then, any assignment I satisfying E ′ (and not assigning x) can be extended to an assignment satisfying E.

PROOF: We have to extend I to satisfy the whole E. In fact we only need to set the value of x. Let us partition the multiset (E - E ′ ) (multiset of clauses that contain the variable x) into two multisets: (E -E ′ )T the multiset already satisfied by I, and (E -E ′ )F the multiset such that the partial assignment I doesn't satisfy any of the clauses. Our aim is to show that the intersection of all the supports of x in (E -E ′ )F is nonempty. This way we will extend I by assigning x to a value in the intersection of all the supports.

Since E is saturated, for every pair of clauses C1 = S:x∨A and C2 = S ′ :x ∨ B in (E - E ′ )F either condition i) or ii) of the definition happens. Condition i) cannot happen because C1 and C2 cannot both be in (E -E ′ )F . Therefore, for every pair of clauses, C1 = S:x ∨ A and C2 = S ′ :x ∨ B in (E - E ′ )F , S ∩S ′ = S or S ∩S ′ = S ′ . Now, we order all the supports of x appearing in (E -E ′ )F in decreasing order of their cardinality. It is straightforward to see that every support is contained or equal to its predecessor. Particularly, the last support is equal to the intersection of all the supports, and it is non-empty.

Theorem 17 (Completeness) For any multiset of clauses C, we have

where D is a satisfiable multiset of clauses, and m is the minimum number of unsatisfied clauses of C.

PROOF: Let x1, . . . , xn be any list of the variables of C. We construct two sequences of multisets C0, . . . , Cn and D1, . . . ,Dn such that

1. C = C0,
2. for i = 1, . . . , n, Ci ∪Di is a saturation of Ci-1 w.r.t. xi, and
3. for i = 1, . . . , n, Ci is a multiset of clauses not containing x1, . . . , xi, and Di is a multiset of clauses containing the variable xi.

By lemma 15, this sequences can effectively be computed: for i = 1, . . . , n, we saturate Ci-1 w.r.t. xi, and then we partition the resulting multiset into a subset Di containing xi, and another Ci not containing this variable.

Notice that, since Cn does not contain any variable, it is either the empty multiset ∅, or it only contains (some) empty clauses { , . . . , }.

Now we are going to prove that the multiset D = ⋃ni=1 Di is satisfiable by constructing an assignment satisfying it. For i = 1, . . . , n, let Ei = Di ∪ . . . ∪ Dn, and let En+1 = ∅. Notice that, for i = 1, . . . , n,

1. the multiset Ei only contains the variables {xi, . . . , xn},
2. Ei is saturated w.r.t. xi, and
3. Ei decomposes as Ei = Di ∪ Ei+1, where all the clauses of Di contain xi and none of Ei+1 contains xi.

Now, we construct a sequence of assignments I1, . . . , In+1, where In+1 is the empty assignment, hence satisfies En+1 = ∅. Now, Ii is constructed from Ii+1 as follows. Assume by induction hypothesis that Ii+1 satisfies Ei+1. Since Ei is saturated w.r.t. xi, and decomposes into Di and Ei+1, by lemma 16, we can extend Ii+1 with an assignment for xi to obtain Ii satisfy Ei. Iterating, we get that I1 satisfies E1 = D = ⋃ni=1 Di.

Concluding, since by the soundness of the rule (Theorem 13) the inference preserves the number of falsified clauses for every assignment, m = |Cn| is the minimum number of unsatisfied clauses of C.

4 Global Consistency inWCSP

From the proof of Theorem 17, we can extract the following exact algorithm for solving WCSP.

I := I ∪ [xi ↦→ extension(xi, I,Di)]

input: AWCSP instance P C0 := signed encoding(P) for i := 1 to k C := saturation(Ci-1, xi) 〈Ci,Di〉 := partition(C, xi) endfor m := |Ck| I := ∅ for i := k downto 1 output: m, I

Given an initial WCSP instance P with k variables, this algorithm returns the minimal cost m of P and an optimal solution I.

The function saturation(Ci-1, xi) computes a saturation of Ci-1 w.r.t. xi applying the resolution rule resolving x until it gets a saturated set. Lemma 15 ensures that this process terminates, in particular that it does not cycle. As we have already said, the saturation of a multiset is not unique, but the proof of Theorem 17 does not depend on which particular saturation we take.

The function partition(C, xi) computes a partition of C, already saturated, into the subset of clauses containing xi and the subset of clauses not containing xi.

The function extension(xi, I,Di) computes an assignment for xi extending the assignment I, to satisfy the clauses of Di according to Lemma 16. The function filters all clauses of Di that are not satisfied by I. Then it computes the intersection of the supports for xi of all of them, and returns one of the values of such an intersection. It returns a value from

The argumentation of the proof of Lemma 16 ensures that this intersection is not empty.

The order on the saturation of the variables can be freely chosen, i.e. the sequence x1, . . . xn can be any enumeration of the variables.

A similar approach to this algorithm was defined using bucket elimination [Dechter, 1999]. Even though both procedures have the same exponential worst-case complexity, we believe that our algorithm can give rise to a better performance profile, in the sense that our computation of the joint operation is incremental.

5 Local Consistency inWCSP

In WCSP a number of local consistency properties have been proposed. These local properties do not ensure the global consistency of a set of constraints. However, they can be enforced very efficiently and used to find a lower bound of the cost.

In this section we focus on binary WCSP instances as in [Larrosa and Schiex, 2003; de Givry et al., 2005]. We assume the existence of a unary constraint for every variable xi. If no such a constraint is defined, we can always define a dummy constraint as f(ak) = 0 for every ak ∈ d(xi). We will use the standard notation for binary WCSP in the literature: Ci will denote a unary constraint over a variable xi, and Cij will denote a binary constraint between variables xi and xj; Ci(ak), where ak ∈ d(xi), will denote f(ak), and Cij(ak, bl), where ak ∈ d(xi) and bl ∈ d(xj), will denote f (ak, bk).

Definition 18 Variable xi is node consistent if there exists a value ak ∈ d(xi) such that Ci(ak) = 0. A WCSP is node consistent (NC∗ ) if every variable is node consistent.

Definition 19 Given a binary constraint Cij , the value b ∈ d(xj) is a simple support for a ∈ d(xi) if Cij(a, b) = 0, and is a full support if Cij(a, b) +Cj(b) = 0

Definition 20 Variable xi is arc consistent if every value a ∈ d(xi) has a simple support in every constraint Cij. A WCSP is arc consistent (AC∗ ) if every variable is node and arc consistent.

Definition 21 Variable xi is full arc consistent if every value a ∈ d(xi) has a full support in every constraint Cij . A WCSP is full arc consistent (FAC∗) if every variable is node and full arc consistent.

Definition 22 Let > be a total ordering over the variables of a WCSP. Variable xi is directional arc consistent (DAC) if every value a ∈ d(xi) has a full support in every constraint Cij such that xj > xi. It is full directional arc consistent (FDAC) if, in addition, every value a ∈ d(xi) has a simple support in every constraint Cij such that xj < xi. A WCSP is full directional arc consistent (FDAC∗) if every variable is node and full directional arc consistent.

Definition 23 Let > be a total ordering over the variables of a WCSP. Variable xi is existential arc consistent if there is at least one value a ∈ d(xi) such that Ci(a) = 0 and has a full support in every constraint Cij . A WCSP is existential arc consistent (EAC∗) if every variable is node and existential arc consistent. A WCSP is existential directional arc consistent (EDAC∗) if it is FDAC∗ and EAC∗ .

In what follows we define four sound inference rules for a sublanguage of signed formulas. We just consider clauses with at most two literals and whose signs are complements of singletons. This language captures binary WCSP instances. As we will see bellow, the rules enforce some known local consistency properties. For lack of space we do not show how these rules may be derived from the signed Max-SAT resolution rule.

In the next rules we assume that N = {i1, . . . , in} = {j1, . . . , jn} and j ∈ N.

Rule 1:

Rule 3:

Rule 4:

PROOF: Say xi is a variable of a WCSP that is not star node consistent. Then for every j ∈ N, Ci(j) > 0. Let be w = min{Ci(j) | j ∈ N} and k such that Ci(k) = w. This means that in the corresponding signed encoding we have Ci(j) copies of {j}:xi, for all j ∈ N. Rule 1 applied to the encoding w many times will remove w copies of {j}:xi, for all j ∈ N, hence all the copies of {k}:xi. Therefore, the WCSP equivalent to the new encoding has the star node consistency property of the variable xi.

Lemma 25 Arc consistency (AC*) can be enforced applying rule 2.

PROOF: Say xi is a variable that is not arc consistent with respect to a constraint Cij , for some variable xj . This means that there is a value a ∈ N such that for all b ∈ N, Cij(a, b) > 0. Let be w = min{Cij(a, b) | b ∈ N}. The constrain Cij will generate among others Cij(a, b) copies of {a}:xi ∨ {b}:xj , for every b ∈ N. Applying rule 2 w many times, we substitute these clauses by w copies of {a}:xi and Cij(a, b) - w copies of {a}:xi ∨ {b}:xj , for every b ∈ N. Since there is one value k such that Cij(a, k) -w = 0, this new set of clauses indicates that now variable xi is arc consistent with respect to Cij , for the value a. Arc consistency for other values would be obtained in the same way.

The previous two lemmas where proved for domains of size two in [Larrosa and Heras, 2005].

Lemma 26 Fixed a total ordering > on the variables, Directional Arc Consistency (DAC) can be enforced from rule 3 applied with the restriction x > y.

PROOF: Let > be a total ordering on the variables. Say xi is a variable that is not directional arc consistent with respect to a restriction Cij for some variable xj where xj > xi. This means that there is a value a ∈ N such that for all b ∈ N, Cij(a, b) + Cj(b) > 0. Suppose that there is some b such that Cij(a, b) = 0, otherwise we can use rule 2 to enforce arc consistency. W.l.o.g. suppose that, for s ∈ {k . . . n}, Cij(a, s) = 0. So, for the same subdomain, Cj(s) > 0. This ensures that we have the following subset of clauses {{a}:xi ∨ {1}:xj, . . . , {a}:xi ∨ {k -1}:xj, {k}:xj, . . . , {n}:xj}. Rule 2 allows us to substitute this set of clauses by {{a}:xi} ∪ ⋃c̸=a,b∈{1...k-1} {{c}:xi ∨ {b}:xj}. Applying rule 3 repeatedly the values {k . . . n} of xj become the full support for xi.

Rule 4 enforces DAC∗ , since it combines DAC and NC∗ . Rule 3 also enforces full arc consistency (FAC∗), but then it must be applied without the limitation x > y.

Existential Arc Consistency (EAC∗) can also be obtained from rule 3 but with different limitations than DAC∗ (in order to avoid cycles).

Example 27 Figure 2 shows a sequence of equivalent signed Max-SAT instances obtained by applying rules 1, 2 and 3.

The sequence of transformations is: a) original formula, b) application of rule 1 to clauses 1, 3 and 5, c) application of rule 2 substituting clauses 8, 9 and 10 by clause 12, d) application of rule 3 substituting clauses 6, 7 and 12 by 13, 14 and 15, and e) application of rule 1 to clauses 2, 4 and 13. The minimal cost is 2. The corresponding sequence of WCSP instances is: a) original instance, b) is NC* but not AC*, c) is AC* but not DAC*, d) is DAC* but not NC* and e) is DAC* and NC*.

6 Conclusions

We have proved that the logic of signed CNF formulas provides the underlying logic of WCSP. On the one hand, this language allows a compact and natural representation of WCSP with not only binary but n-ary constraints. On the other hand, the inference system captures and formalizes the algorithms for global as well as local consistency that have been described in the WCSP community.

We are currently investigating new derived rules that could be applied in polynomial time and enforce stronger forms of soft local consistency.