Exploiting Inference Rules to Compute Lower Bounds for MAX-SAT Solving

1 Introduction

In the past few years MAX-SAT solving techniques have drawn increasing attention [Gramm et al., 2003; de Givry et al., 2003; Alsinet et al., 2003; Shen and Zhang, 2004; Li et al., 2005; 2006; Larrosa and Heras, 2005; Xing and Zhang, 2005; Heras and Larrosa, 2006] in various fields of artificial intelligence, because many problems can be handled by transforming an original problem instance into a MAXSAT instance and solving it with a MAX-SAT solver. These problems include MAX-CUT, MAX-CLIQUE, as well as problems in domains such as routing [Xu et al., 2003], bioinformatics [Strickland et al., 2005], scheduling [Vasquez and Hao, 2001], and probabilistic reasoning [Park, 2002].

MAX-SAT is an optimization version of the SAT problem. In the last decade significant progress has been made in the performance of SAT solvers. A modern SAT solver can handle instances containing up to a million variables within rea-

∗This work has been supported by the Australian Research Council grant DP0452628, National Basic Research 973 Program of China under grant 2005CB321902, National Natural Science Foundation of China grants 60496327, 10410638 and 60473004, and Guangdong Provincial Natural Science Foundation grants 04205407 and 06023195.

†Corresponding author sonable time [Kautz and Selman, 2005]. Almost every complete SAT solver is based on the DPLL algorithm [Davis et al., 1962], and almost every DPLL-based solver employs transformation rules, such as unit propagation and resolution, to achieve high efficiency. Such rules improve SAT solvers in two main aspects. First, it may be used to simplify a formula. Second, at each internal node of the search tree, the solver may attempt to use such rules to prove unsatisfiability of the formula instantiated by a partial assignment, and if the formula is really unsatisfiable, the solver will not extend the partial assignment any more. Although such rules are of great use in SAT solving, it can not be applied directly to MAXSAT solvers for several reasons. First, using these rules to simplify a formula may not preserve the optimal value. Second, since the goal of a MAX-SAT solver is to find maximum number of satisfied clauses, the proof of unsatisfiability is meaningless. This is why there is a big gap between SAT and MAX-SAT solving. Fortunately, transformation rules can be used to compute lower bounds during the MAX-SAT searchtransformation rules for (weighted) MAX-SAT and propose several new rules to improve the lower bounds.

Due to the differences between the logic behind the MAXSATproblemand that behindSAT, [Larrosa andHeras, 2005] developed a logical framework to extend the SAT solving techniques to MAX-SAT. However, because of the simplicity of this framework, we can not study the properties of the transformation rules intensively. In order to avoid this limitation, we extend the framework by introducing several new fundamental concepts.

This paper is organized as follows. In Section 2, we describe our logical framework for MAX-SAT, and intensively study the properties of inference rules. In Section 3, we propose several new inference rules to improve MAX-SAT solvers. In Section 4, as a case study, we show how to exploit inference rules to improve the lower bound function of MAX-2-SAT. Section 5 shows experimental results. Finally we conclude the paper in Section 6.

2 A Logical Framework forWeighted MAX-SAT

In this section, we propose a logical framework for weighted MAX-SAT, which is more general and suitable for studying the MAX-SAT solving techniques than the one proposed in [Larrosa and Heras, 2005; Heras and Larrosa, 2006].

2.1 Basic Notation and Definitions

For convenience we introduce some notation and definitions. In propositional logic, a variable x may take values 1 (for true) or 0 (for false). A literal is either a variable or its negation. The variable related to literal l is denoted by var(l). The negation of a variable (or literal) x is denoted by ¯x. A clause C = l1 ∨ l2 ∨ . . . ∨ lm is a disjunction of literals in which no variable occurs more than once. A weighted clause is a pair (C, w) where C is a clause and w is the weight of this clause. Without loss of generality, we assume w is a natural number in this paper. A CNF formula is a conjunction of clauses. A weighted CNF formula is a set of weighted clause. A bounded formula is a pair (F, k) where F is a weighted CNF formula and k, a natural number, is the upper bound of this formula. For a formula F over a variable set V , an assignment for F is a mapping from V ′ to {0, 1} and is denoted by a vector ⃗X ∈ {0, 1}n, where n is the number of variables in V ′ . The assignment is complete if V ′ ⊇ V ; otherwise it is partial. An assignment satisfies a clause if it satisfies at least one literal in the clause. An assignment satisfies a CNF formula if it satisfies every clause in the formula. The instantiation of a formula F by forcing literal l to be true, denoted by F[l], produces a new formula as follows: all clauses containing literal l are eliminated, and ¯l is deleted from each clause where it occurs. We use ✷ to denote empty clause, which can not be satisfied by any assignment.

Given a weighted CNF formula F and a complete assignment ⃗X for F , we set

which indicates the cost of ⃗X in F .

Given a weighted formula F, weighted MAX-SAT problem is to find an assignment ⃗X such that COST(F, ⃗X) is minimum. We denote such minimal value by OPT(F). Since unweighted MAX-SAT problem is a particular case in which w = 1 for every weighted clause (C, w) in F , we only consider weighted MAX-SAT problem in this paper.

2.2 The Logical Framework

Definition 1 A complete assignment ⃗X is called a model of a bounded formula (F, k), if COST(F, ⃗X) < k. A bounded formula is unsatisfiable if it has not any model.

Obviously, (F, 0) is unsatisfiable for any weighted formula F and if (✷, k) ∈ F , then (F, k) is also unsatisfiable.

Note that in the above definition, if k = 1, then a model should satisfy every clause in the formula, which is the same as the case in the context of SAT problem. So SAT solving can be considered as a special case in our logical framework.

According to Definition 1, we can naturally generalize semantic entailment relation and equivalence relation from classical positional logic to our logical framework.

Definition 2 Given two bounded formulas (F1, k1) and (F2, k2),

holds 1 if every model of (F1, k1) is also a model of (F2, k2). (F1, k1) and (F2, k2) are equivalent, denoted by (F1, k1) ≡ (F2, k2), if (F1, k1) |= (F2, k2) and (F2, k2) |= (F1, k1).

Definition 3 Given two weighted CNF formulas F1 and F2,

holds, if (F1, k) |= (F2, k) for any k. Two weighted CNF formulas F1 and F2 are equivalent, denoted by F1 ≡ F2, if F1 |= F2 and F2 |= F1.

The following proposition and corollary reveal the relation between our definitions and the weighted MAX-SAT problem.

Lemma 1 Let F1 and F2 be weighted CNF formulas, F1 |= F2, if and only if for every complete assignment ⃗X of F1 and F2, we have

Proposition 1 Given two weighted CNF formulas F1 and F2, if F1 |= F2, then OPT(F1) ≥ OPT(F2).

Corollary 1 Given two weighted CNF formulas F1 and F2, if F1 ≡ F2, then OPT (F1) = OPT (F2).

Now we describe the procedure MAX-DPLL, which is slightly different from [Larrosa and Heras, 2005], for solving weighted MAX-SAT as follows.

function MAX-DPLL((F, k):bounded formula):interger;

1. F:=ApplyEquivalentRules((F, k));
2. F ′ :=ApplyNonequivalentRules((F, k));
3. if (✷, k) ∈ F ′ then return k;
4. if F = ∅ then return 0;
5. if F = {(✷,w)} then return w;
6. l:=SelectLiteral(F);
7. v:=MAX-DPLL((F[l], k));
8. v:=MAX-DPLL((F[¯l], v));
9. return v;

end function

Procedure 1: The procedure for solving weighted MAX-SAT.

The MAX-DPLL procedure is much like the DPLL, and its correctness is derived from the recursive equation

The sub-procedures ApplyEquivalentRules and ApplyNonequivalentRules in lines 1 and 2 will be discussed later. For the moment, they can be considered as procedures just returning the input formula F. The initial value of variable k, upper bound of formula F , can be obtained by running a local search procedure, such as [Borchers and Furman, 1999].

1 Of course we can generalize this definition by replacing (F1, k1) with more than one bounded formula, but it is meaningless in the context of MAX-SAT solving.

Now let's pay attention to inference rules for weighted MAX-SAT. An inference rule is in this form:

where P and Q are weighted CNF formulas. The procedure for applying an inference rule to a formula can be described as follows (WCF is short for weighted CNF formula):

function ApplyRule(P ⇒ Q:inference rule, F :WCF):WCF;

2. return F;

end function

Procedure 2: The procedure for applying an inference rule to a weighted CNF formula.

Definition 4 An inference rule P ⇒ Q is sound if for any weighted CNF formula R, we have OPT(P ∪ R) = OP T (Q ∪ R).

An inference rule P ⇒ Q is an equivalent rule if P ≡ Q. The following proposition shows that applying equivalent rules to a formula can preserve its optimal value.

Proposition 2 All equivalent rules are sound.

For a bounded formula (F, k), [Larrosa and Heras, 2005; Heras and Larrosa, 2006] incorporated the following inference rules into their weighted MAX-SAT solvers:

• BR1: {(A, k), (A ∨ B, w)} ⇒ {(A, k)}
• BR2: {(A,w), (A, u)} ⇒ {(A,w⊕u)}
• BR3: If w ⊕ u = k then {(A,w), (A ∨ B, u)} ⇒ {(A, w), (A ∨ B, k)}
• BR4: {(A, 0)} ⇒ { }
• RES: {(x ∨ A, u), (¯x ∨ B, w)} ⇒ {(A ∨ B, m), (x ∨ A, u ⊖ m), (¯x ∨ B, w ⊖ m), (x ∨ A ∨ ¯B, m), (¯x ∨ ¯ A ∨ B, m)}

where x is any literal, A and B are arbitrary disjunction of literals, m = min{u,w} in the RES rule, and operators ⊕ and ⊖ are defined as

Note that [Larrosa and Heras, 2005; Heras and Larrosa, 2006] incorporated some special cases of RES rather than the general RES rule.

By exploiting the above rules, [Heras and Larrosa, 2006] implemented a weighted MAX-SAT solver that outperforms other state-of-art solvers. However, we can observe that all the above rules are equivalent rules. It is no doubt that equivalent rules are sound, that is, preserve the model and the optimal value, so it is safe to exploit equivalent rules to produce a new formula. But if we only consider such rules, very few rules can be exploited.

An alternative way is to choose rules in this form P ⇒ Q such that OPT(P) = OPT(Q). Unfortunately, applying such kind of rules is not safe, because OPT (P ) = OPT (Q) does not ensure the validity of OP T (P ∪R) = OP T (Q∪R) where P, Q, and R are weighted CNF formulas. A counter example is given as follows.

Thus, if we attempt to incorporate more inference rules to weighted MAX-SAT solvers, we should find rules that are not necessarily equivalent but can preserve the optimal value of the original formula. For this purpose, we introduce the following definition.

Definition 5 Let Λ be a non-empty set of variables, two weighted CNF formulas F1 and F2 are said to be Λequivalent, denoted by F1 ≈Λ F2, if for every weighted CNF formula P over Λ, F1 |= P if and only if F2 |= P. An inference rule P ⇒ Q is a Λ-equivalent rule if P ≈Λ Q.

For Λ-equivalent rules, we have the following proposition and theorem.

Proposition 3 All equivalent rules are Λ-equivalent for any Λ.

Theorem 1 If P ⇒ Q is a Λ-equivalent rule, and R is a weighted CNF formula over Λ, then OPT(P ∪ R) = OP T (Q ∪ R).

Theorem 1 gives the condition under which we can apply Λ-equivalent rules to the formula. And Proposition 3 shows that Λ-equivalent is a weaker notation than equivalent, that is, the set of equivalent rules is the subset of the set of Λequivalent rules. So, theoretically, considering Λ-equivalent rules will provide more choices than considering equivalent rules only. Thus, it is promising to employ Λ-equivalent rules in weighted MAX-SAT solvers. In Section 3, we will propose several Λ-equivalent rules.

Now let us pay attention to nonequivalent rules which are neither equivalent nor Λ-equivalent. We note that every inference rule P ⇒ Q considered in this paper should satisfy P |= Q. So although applying a nonequivalent rule to a formula may not preserve its optimal value, we may exploit it to compute a lower bound. From Proposition 1, we can conclude that lower bounds that are computed in this way are admissible, namely the lower bound is always less than or equal to the optimal value. In fact, sometimes it is easier to use nonequivalent rules to obtain conflict clauses. For example, [Shen and Zhang, 2004; Li et al., 2005] apply inference rules like {(¯x, 1), (x ∨ y, 1), (¯ y, 1)} ⇒ {(✷, 1)}. However, since such rules are not equivalent, they can not be used to achieve a tight lower bound usually. In Section 4, we will discuss this problem.

3 Some Λ-Equivalent Inference Rules

In this section we present two Λ-Equivalent Rules and show in which situation they can be applied.

The first Λ-equivalent rule we propose is

where x is a literal, and A and B are arbitrary clauses (may be empty).

Theorem 2 Let Λ be a non-empty set of variables. If var(x) /∈ Λ, then 1-RES is a Λ-equivalent rule.

Proof Without loss of generality, we may consider A and B as variables. It is easy to verify that {(x ∨ A, u), (¯x ∨ B,w)} |= {(A ∨ B,min{u,w})}, so for any weighted formula P, whenever {(A∨B, min{u, w})} |= P , we also have {(x∨A, u), (¯x∨B, w)} |= P . Now suppose {(x∨A, u), (¯x∨ B, w)} |= P, where P is a weighted formula not containing x. There are four cases.

• Case 1: A = 0 and B = 0, if x = 0, the cost is u, otherwise the cost is v, from Lemma 1, the cost of P in this case should be less than min{u, v}, which is not greater than the formula {(A ∨ B,min{u,w})} in this case.
• Case 2: A = 0 and B = 1, if x = 0 the cost is u, otherwise is 0, from Lemma 1, the cost of P should be 0, which is also not greater than {(A∨B, min{u, w})}.
• Case 3: A = 1 and B = 0, analysis is similar with above cases.
• Case 4: A = 1 and B = 1, analysis is similar with above cases.

To sum up, we can conclude that no matter in which case, the cost of P is less than or equal to {(A∨B,min{u,w})}, so we also have {(A ∨ B, min{u, w})} |= P . □

According to Theorem 1 and Theorem 2, if a formula F contains (x ∨ A, u) and (¯x ∨ B,w), and var(x) does not occur in other clauses in F, we can apply 1-RES to F .

Example 2 Let F = {(x ∨ y, 2), (¯x ∨ z, 3)}. If we apply the RES rule, we will get {(y∨z, 2), (¯x∨z, 1), (x∨y∨¯ z, 2), (¯x∨ ¯ y∨z, 2)}, which is too complicated. But if we apply the 1-RES rule, we will get a much simpler formula {(y ∨ z, 2)}.

The second Λ-equivalent rule we propose is

where x and y are literals, and A is the conjunction of arbitrary literals (may be empty).

Note that we can apply the RES rule to the right side of the 2-RES rule to get simpler formula further.

Theorem 3 Let Λ be a non-empty set of variables. If var(x) /∈ Λ, then 2-RES is a Λ-equivalent rule.

Proof The proof is similar with Theorem 1, so we omit it here. ✷

According to Theorem 1 and Theorem 3, if a formula F contains {(x, u), (x ∨ y, v), and (¯x ∨A, w), and var(x) does not occur in other clauses in F, we can apply 2-RES to F .

2 This rule can be considered as an extension of the elimination rule [Bansal and Raman, 1999] to weighted MAX-SAT.

Example 3 Let F = {(x, 3), (x ∨ y, 2), (¯x ∨ z, 1), (¯ z, 1)}. The 2-RES rule transforms F into {(y ∨ z, 1), (¯ y ∨ z, 1), (¯ z, 1)}. And the RES rule transform the resulting formula into {(z, 1), (¯ z, 1)}, which can be simplified to {✷, 1}.

4 ANew Lower Bound Function for MAX-2-SAT

MAX-2-SAT is a special case of weighted MAX-SAT, in which each clause has weight 1 and at most two literals. [Shen and Zhang, 2004] studied several lower bound functions for MAX-2-SAT, and proposed a lower bound function lower bound4a, which is proved to be admissible and consistently better than others. The procedure for calculating this function is as follows (LB1 is the number of conflicting (or empty) clauses by the current partial assignment).

function lower bound4a(i:integer):integer;

1. LB4:=LB1;
2. while (i ≤ n) do
3. LB4:=LB4+min(μ(¯i),μ(i));
4. t := |μ(¯i) - μ(i)|;
5. if μ(¯i) > μ(i) then Y := B(i) else Y := B(¯i);
6. S := φ;
7. for j ∈ Y if (t > 0) do
8. if (μ(j) > μ(¯j)) then S := S ∪ {j} else
9. t := t -1; μ(j) := μ(j) + 1;
10. end if
11. end for
12. for j ∈ S if (t > 0) do
13. t := t -1; μ(j) := μ(j) + 1;
14. end for
15. i := i +1;
16. end while
17. return LB4;

end function

Procedure 3: The procedure for computing LB4a.

The main idea of this procedure is to exploit the inference rule {(¯x, 1), (x ∨ y, 1), (¯ y, 1)} ⇒ {(✷, 1)} to obtain a lower bound (Due to limited space, for more details, please refer to the original paper). However, this rule is not equivalent, so the tight may be not tight enough. According to the RES rule, {(¯x, 1), (x ∨ y, 1), (¯ y, 1)} ≡ {(¯x ∨ ¯ y), (✷, 1)}, so we exploit the rule {(¯x, 1), (x ∨ y, 1), (¯ y, 1)} ⇒ {(¯x ∨ ¯ y, 1), (✷, 1)} to get a better lower bound. Procedure 4 illustrates our algorithm. Line 12 and 17 change the formula by deleting x ∨ y and adding the clause ¯x∨ ¯ y. k can be considered as a constant number, in our code, we choose k = 3. So the time complexity of lower bound5 is the same as lower bound4a. In order to compare with lower bound4a, we write the pseudo code in the same style as procedure 3. Note that the real code is far from this pseudo code.

function lower bound5(i, k:integer):integer;

1. LB5:=LB1; 2. i1 := i; 3. while (k > 0) do 4. while (i ≤ n) do 5. LB5:=LB5+min(μ(¯i),μ(i)); 6. t := |μ(¯i) -μ(i)|; 7. if μ(¯i) > μ(i) then Y := B(i) else Y := B(¯i); 8. S := φ; 9. for j ∈ Y if (t > 0) do 10. if (μ(j) > μ(¯j)) then S := S ∪ {j} else 11. t := t -1; μ(j) := μ(j) + 1; 12. B(i) := B(i) - {j}; B(¯i) := B(¯i) ∪ {¯j}; 13. end if 14. end for 15. for j ∈ S if (t > 0) do 16. t := t -1; μ(j) := μ(j) + 1; 17. B(i) := B(i) - {j}; B(¯i) := B(¯i) ∪ {¯j}; 18. end for 19. if μ(¯i) > μ(i) then μ(¯i) := t else μ(i) := t; 20. i := i +1; 21. end while 22. i := i1; k := k -1; 23. end while 24. return LB5; end function

Procedure 4: The procedure for computing LB5.

The following theorem shows that LB5 is admissible and consistently better than LB4a.

Theorem 4 LB4a ≤ LB5 ≤ OPT(F).

5 Experimental Results

The experimental results are presented in this section. Our solver, called Λ-SAT, is compared with the solver Toolbar (http://carlit.toulouse.inra.fr/cgi-bin/awki.cgi/SoftCSP), which implemented by [Larrosa and Heras, 2005; Heras and Larrosa, 2006]. Other solvers are not freely available and [Heras and Larrosa, 2006] showed that Toolbar outperforms others. So we only compare our solver with Toolbar.

Our solver implements the variable selection strategy known as Jeroslow-Wang rule [Jeroslow and Wang, 1990], which is widely employed in state-of-art SAT solvers. For inference rules, we choose the same as [Heras and Larrosa, 2006], additionally we also employ the new rules proposed in this paper. Our tool is implemented in C.

We run two solvers with randomMAX-2-SAT (experimental results are illustrated in Table 1, #var stands for the number of variables and #cls stands for the number of clauses, #node stands for the mean number of nodes of the whole search tree, time stands for the mean running time over 30 instances) and The results demonstrate that for small instances, the performance of the our solver is nearly the same as Toolbar, while for large instances the former outperforms the latter, and especially for some larger instances, our solver can be orders of magnitude faster than Toolbar.

Table 2: The experimental results on randomMAX-3-SAT.

6 Conclusions and Future Work

The main contributions of this paper are in two aspects. First, we develop a general logical framework that is suitable for studying weighted MAX-SAT problem. This is because many concepts in SAT are easy to be extended in our framework. This may provide more chances to extend techniques taken by SAT solvers to MAX-SAT solvers. Second, we propose several new inference rules, which can be exploited to get lower bound of better quality. The experimental results support our conclusion.

For future work, we will further study how to extend SAT techniques to MAX-SAT solver, such as clause learning and restarts. Moreover, for unweighted MAX-SAT, we notice that several lower bound computation techniques [Li et al., 2006], which focus on searching for disjoint inconsistent subformulas, have been proposed. Based on our logical framework, we will attempt to generalize such techniques to compute lower bounds for weighted MAX-SAT efficiently. Recently, a simple model have been presented for generating random weighted MAX-2-SAT instances (http://www.nlsde.buaa.edu.cn/ kexu/benchmarks/max-satbenchmarks.htm). Such instances are transformed from forced satisfiable SAT instances of Model RB [Xu and Li, 2006; Xu et al., 2005] and are, unfortunately, too hard for both toolbar and our solver. We will try to improve our solver to handle these benchmarks within reasonable time.