# an_exact_inference_scheme_for_minsat__e471c0c6.pdf

An Exact Inference Scheme for Min SAT

Chu-Min Li Huazhong Univ. of Science and Technology MIS, Universit e de Picardie Jules Verne

Felip Many a Artiﬁcial Intelligence Research Inst. (IIIA) Spanish National Research Council (CSIC)

We describe an exact inference-based algorithm for the Min SAT problem. Given a multiset of clauses φ, the algorithm derives as many empty clauses as the maximum number of clauses that can be falsiﬁed in φ by applying ﬁnitely many times an inference rule, and returns an optimal assignment. We prove the correctness of the algorithm, describe how it can be extended to deal with weighted Min SAT and weighted partial Min SAT instances, analyze the differences between the Max SAT and Min SAT inference schemes, and deﬁne and empirically evaluate the Min SAT Pure Literal Rule.

1 Introduction

Min SAT is the problem of ﬁnding an assignment that maximizes the number of falsiﬁed clauses (or equivalently, minimizes the number of satisﬁed clauses) in a multiset of clauses, and Max SAT is the problem of ﬁnding an assignment that minimizes the number of falsiﬁed clauses (or equivalently, maximizes the number of satisﬁed clauses). When weights are added to clauses, we refer to these problems as weighted Max SAT/Min SAT. When there are clauses considered to be hard and clauses considered to be soft, we refer to them as (weighted) partial Max SAT/Min SAT. The development of Max SAT solvers incorporating novel and powerful solving techniques [Li and Many a, 2009], as well as the annual celebration of an evaluation of Max SAT solvers [Argelich et al., 2008], have been decisive to consolidate Max SAT-based problem solving as a competitive alternative to solve challenging combinatorial optimization problems [Argelich et al., 2011; Morgado et al., 2013]. Given the success of Max SAT, a number of researchers have started to look into Min SAT in the last ﬁve years. At ﬁrst sight, one could think that the solving techniques and encodings to be used in Min SAT are very similar to the

Research partially supported by the Generalitat de Catalunya grant AGAUR 2014-SGR-118, CSIC Intramural Project 201450E045, and the Ministerio de Econom ıa y Competividad project CO-PRIVACY TIN2011-27076-C03-03. The second author was supported by Mobility Grant PRX14/00195 of the Ministerio de Educaci on, Cultura y Deporte.

ones used in Max SAT and, therefore, that there is no need of investigating Min SAT from a problem solving perspective. However, most of the research conducted so far indicates that they may be quite different, as well as that the performance proﬁle of Max SAT and Min SAT is also different for several optimization problems represented into these formalisms [Argelich et al., 2014; Ignatiev et al., 2014; Li et al., 2012]. All these ﬁndings suggest that it is worth to investigate Min SAT, and ﬁnd out whether it can be used as a generic problem solving approach for optimization problems either separately or in combination with Max SAT. It is also worth mentioning that solving Min SAT is meaningful for both satisﬁable and unsatisﬁable instances, whereas solving Max SAT is only meaningful for unsatisﬁable instances. Let us mention two examples that illustrate some differences between Max SAT and Min SAT. The ﬁrst example is about solvers: In branch-and-bound Min SAT solvers one has to compute, at every node of the search tree, an upper bound on the maximum number of clauses that can be falsiﬁed, and in branch-and-bound Max SAT solvers one has to compute a lower bound on the minimum number of clauses that can be falsiﬁed. While the upper bound is computed using graph-based techniques, the lower bound is computed by applying unit propagation. As a result, for example in [Li et al., 2012], we have that Min SAT greatly outperforms Max SAT on combinatorial auctions and Max Clique instances using solvers sharing many implementation details like Min Satz [Li et al., 2012] and Max Satz [Li et al., 2007; 2010a], despite of the fact that the encodings of such problems are almost identical. The second example is about encodings: Given a Constraint Satisfaction Problem (CSP), one can represent the problem of determining the maximum number of constraints that can be satisﬁed with both Max SAT and Min SAT encodings. Using the Max SAT direct encoding [Argelich et al., 2012], we must add one clause for every no-good, while using the Min SAT direct encoding [Argelich et al., 2013], we must instead add one clause for every good. This implies, for instance, that for representing the constraint X = Y , we need a number of clauses linear in the domain size in Min SAT, and a quadratic number of clauses in Max SAT. We are in the opposite situation if we want to represent the constraint X = Y , So, it seems that Max SAT and Min SAT could be complementary in some scenarios [Argelich et al., 2013].

Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence (IJCAI 2015)

In this paper we focus on inference schemes for Max SAT and Min SAT, and present original contributions to Min SAT. There exists a Max SAT resolution rule (c.f. Section 4) that can also be applied to Min SAT because it preserves the number of falsiﬁed clauses when the premises of the rule are replaced by its conclusions. Besides, there exists also an exact inference algorithm for Max SAT [Bonet et al., 2007] that derives, by applying the Max SAT resolution rule a ﬁnite number of times following a certain strategy, as many empty clauses as the minimum number of clauses that can be falsiﬁed in a multiset of clauses. Nevertheless, it is an open problem to ﬁgure out how an inference rule may be used to compute a Min SAT solution; i.e., to derive as many empty clauses as the maximum number of clauses that can be falsiﬁed. The main objective of this work is to solve that open problem by devising an exact inference algorithm for Min SAT that relies on the existing inference algorithm for Max SAT but contains signiﬁcant differences despite of the fact that both algorithms apply the Max SAT resolution rule. In particular, we describe the algorithm and prove its correctness, show how it can be extended to deal with weighted Min SAT and weighted partial Min SAT instances, analyze the differences between the Max SAT and Min SAT inference schemes, and deﬁne and empirically evaluate the Min SAT Pure Literal Rule. The paper is organized as follows: Section 2 gives basic deﬁnitions. Section 3 summarizes the related work. Section 4 presents the existing inference scheme for Max SAT. Section 5 describes the inference algorithm for Min SAT, and proves its correctness. Section 6 compares the Max SAT and Min SAT inference schemes, and presents new insights into Min SAT. Finally, Section 7 contains the concluding remarks.

2 Preliminaries

A literal is a propositional variable or a negated propositional variable. A clause is a disjunction of literals. A weighted clause is a pair (c, w), where c is a is a disjunction of literals and w, its weight, is a natural number or inﬁnity. A clause is hard if its weight is inﬁnity; otherwise it is soft. A weighted partial Min SAT (Max SAT) instance is a multiset of weighted clauses φ = {(h1, ), . . . , (hk, ), (c1, w1), . . . , (cm, wm)}, where the ﬁrst k clauses are hard and the last m clauses are soft. For simplicity, in what follows, we omit inﬁnity weights, and write φ = {h1, . . . , hk, (c1, w1), . . . , (cm, wm)}. Notice that a soft clause (c, w) is equivalent to having w copies of the clause (c, 1), and that {(c, w1), (c, w2)} is equivalent to (c, w1 + w2). A truth assignment assigns to each propositional variable either 0 or 1. Weighted Partial Min SAT (Max SAT), or WPMin SAT (WPMax SAT), for an instance φ is the problem of ﬁnding an assignment in which the sum of the weights of the satisﬁed (falsiﬁed) soft clauses is minimal, and all the hard clauses are satisﬁed. The Weighted Min SAT (Max SAT) problem, or WMin SAT (WMax SAT), is the WPMin SAT (WPMax SAT) problem when there are no hard clauses. The Partial Min SAT (Max SAT) problem, or PMin SAT (PMax SAT), is the WPMin SAT (WPMax SAT) problem when all the soft

clauses have the same weight. The (Unweighted) Min SAT (Max SAT) problem is the Partial Min SAT (Max SAT) problem when there are no hard clauses.

3 Related Work

The work on Min SAT can be traced back to the mid-90s in the area of approximation algorithms [Kohli et al., 1994; Marathe and Ravi, 1996], but it was not until 2010 that Min SAT started to be studied from a problem solving perspective. The main results of this recent work on Min SAT may be succinctly summarized as follows:

I) Deﬁnition of transformation between Min SAT and Max SAT: Reductions from Min SAT to PMax SAT were deﬁned in [Li et al., 2010b], but they do not generalize to WPMin SAT. This drawback was overcome with the deﬁnition of the natural encoding [K ugel, 2012], which was improved in [Zhu et al., 2012]. Reductions of WPMin SAT to Group Max SAT were evaluated in [Heras et al., 2012].

II) Development of branch-and-bound solvers: The only existing WPMin SAT solver, Min Satz [Li et al., 2011; 2012], is based on Max Satz [Li et al., 2007], and implements upper bounds that exploit clique partition algorithms and Max SAT technology.

III) Development of SAT-based solvers: There exist two WPMin SAT solvers of this class [Ans otegui et al., 2012; Heras et al., 2012]. The main difference with SAT-based Max SAT solvers lies in the way of relaxing soft clauses.

IV) Deﬁnition and evaluation of genuine Min SAT encodings of relevant problems such as weighted Max CSP [Argelich et al., 2013; 2014], and graph problems [Ignatiev et al., 2014; 2013].

4 Inference in Max SAT

The classical resolution rule x A, x B A B (where x is a variable, and A and B are disjunctions of literals) is unsound for Max SAT. It works by adding the conclusion of the rule to the premises, and this may increase the number of falsiﬁed clauses in the derived instance. In contrast, the Max SAT resolution rule works by replacing the premises by its conclusions in such a way that the number of falsiﬁed clauses is preserved for every assignment. The Max SAT resolution rule is deﬁned as follows [Bonet et al., 2007; Larrosa et al., 2008]:

x a1 . . . as x b1 . . . bt a1 . . . as b1 . . . bt x a1 . . . as b1 x a1 . . . as b1 b2 x a1 . . . as b1 . . . bt 1 bt x b1 . . . bt a1 x b1 . . . bt a1 a2 x b1 . . . bt a1 . . . as 1 as

input: C C0 := C for i := 1 to n C := saturation(Ci 1, xi) Ci, Di := partition(C, xi) endfor m := |Cn| I := for i := n downto 1 I := I [xi 7 max extension(xi, I, Di)] output: m, I

Figure 1: An exact inference algorithm for Max SAT

The tautologies concluded are removed, and repeated literals in a clause are collapsed into one. We say that the rule cuts the variable x. [Bonet et al., 2006; 2007] proved that the Max SAT resolution rule is sound and complete. It is sound because the number of clauses that every assignment falsiﬁes in the premises is the same as the number of clauses that it falsiﬁes in the conclusions. It is complete because, for every multiset of clauses C whose minimum number of falsiﬁed clauses is m, the application of the rule (ﬁnitely many times) following a strategy explained below derives a multiset formed by exactly m empty clauses. Before describing the exact inference algorithm for Max SAT of [Bonet et al., 2007], we need two deﬁnitions:

Deﬁnition 1 We write C D when the multiset of clauses D can be obtained from the multiset C by applying the Max SAT resolution rule a ﬁnite number of times. We write C x D when this sequence of applications only cuts the variable x.

Deﬁnition 2 A multiset of clauses C is said to be saturated w.r.t. the variable x if, for every pair of clauses c1 = x A and c2 = x B of C, after applying the Max SAT resolution rule, there is a literal l such that l is in A and l is in B. 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 by applying the inference rule cutting x ﬁnitely many times.

Trivially, by the previous deﬁnition, a multiset of clauses C is saturated w.r.t. x iff every possible application of the inference rule cutting x only introduces clauses containing x due to the fact that the ﬁrst clause in the conclusions is a tautology and, therefore, is eliminated. Although every multiset of clauses is saturable, its saturation is not unique. For instance, the multiset {x1, x1 x2, x1 x3} has two possibles saturations w.r.t. variable x1: the multiset {x2, x2 x3, x1 x2 x3, x1 x2 x3}, and the multiset {x3, x2 x3, x1 x2 x3, x1 x2 x3}. Nevertheless, the algorithm described below is correct independently of the saturation selected. Figure 1 gives the pseudo-code of the exact inference algorithm for Max SAT. Given an input multiset of clauses C with n different variables, the algorithm returns the minimum number m of clauses of C that can be falsiﬁed, and an optimal Max SAT assignment I.

Function saturation(C, x) computes a saturation of C w.r.t. x. The order in which the algorithm computes the saturation of the variables can be freely chosen; i.e., the sequence x1, . . . xn can be any enumeration of the variables. Function partition(C, xi) computes a partition of C into the multiset Ci of clauses without occurrences of the variable xi, and the multiset Di of clauses with occurrences of xi. Function max extension(xi, I, Di) computes a truth assignment for xi as follows: if I satisﬁes all the clauses in Di, including the case in which Di = {}, then the function returns false (xi is set to false); otherwise, either all the clauses of the form xi A are satisﬁed or all the clauses of the form xi B are satisﬁed. In this case, xi is set in such a way that all the clauses in Di become satisﬁed. The algorithm has two parts. In the ﬁrst part, the algorithm successively saturates w.r.t. all the variables occurring in the input multiset. Once the current multiset is saturated w.r.t. the variable under consideration, say xi, it partitions the resulting multiset into two multisets: Ci and Di. Ci contains the clauses without occurrences of xi, and Di contains the clauses with occurrences of xi. The algorithm continues saturating Ci w.r.t. one of the remaining variables, and ignores Di. This process continues until all the variables are eliminated. At the end, Cn contains no variables, and the number of empty clauses in Cn is the returned minimum number of falsiﬁed clauses. In the second part, the algorithm builds an optimal assignment taking into account the information in Di. Every optimal assignment must satisfy all the derived Di s.

Example 1 Let φ = {x1, x1 x2, x1 x3, x3}. Resolving the ﬁrst two clauses, we get {x2, x1 x2, x1 x3, x3}. Resolving the second and third clause, we get a saturation of φ w.r.t. x1: {x2, x2 x3, x1 x2 x3, x1 x2 x3, x3}. Hence, C1 = {x2, x2 x3, x3}, and D1 = {x1 x2 x3, x1 x2 x3}. Resolving the ﬁrst two clauses of C1, we get {x3, x2 x3, x3}, which is a saturation of C1 w.r.t. x2. Hence, C2 = {x3, x3}, and D2 = {x2 x3}. Resolving {x3, x3}, we get the empty clause. Hence, C3 = { }, and D3 = {}. So, the minimum number of falsiﬁed clauses is 1, and x3 7 false, x2 7 false, x1 7 true is an optimal assignment.

5 Inference in Min SAT

The goal of an exact Min SAT algorithm is to compute an assignment that falsiﬁes the maximum number of clauses in a Min SAT instance. In this section we deﬁne an algorithm that derives, by applying the Max SAT resolution rule, as many empty clauses as the maximum number of clauses that can be falsiﬁed. First of all, we should note that the Max SAT resolution rule is also a sound inference rule for Min SAT because its application preserves the number of falsiﬁed clauses. Nevertheless, to get completeness we need a different strategy of applying the rule, and a new way of deriving an optimal assignment. In our approach, given a variable xi occurring in the Min SAT instance φ under consideration, we start by computing a saturation w.r.t. xi. By the soundness of resolution, the number of clauses that an assignment falsiﬁes in φ and in the computed saturation is the same. We then partition the saturation

into two multisets as in Max SAT: the multiset Ci of clauses without occurrences of the variable xi, and the multiset Di of clauses with occurrences of xi. In the next step, in contrast to Max SAT where a saturation of Ci w.r.t. xi+1 is computed, we now compute a saturation of the Min SAT instance φ formed by both Ci and the multiset of clauses, say Fi, resulting of eliminating all the occurrences of the literals xi and xi in Di; i.e., Fi := {A | xi A Di} {B | xi B Di}. As we show in the following lemma, the Min SAT problem for φ can be reduced to the Min SAT problem for φ = Ci Fi.

Lemma 1 Let φ be a Min SAT instance, and let φ be a Min SAT instance derived from φ by ﬁrst computing a saturation Ci Di of φ w.r.t. a variable xi occurring in φ, and then removing from Di all the occurrences of both xi and xi. We write φ = Ci Fi = Ci {A | xi A Di} {B | xi B Di}. If I is an optimal assignment of φ, then I is also an optimal assignment of φ and falsiﬁes the same number of clauses in φ and φ .

Proof Since every assignment falsiﬁes the same number of clauses in φ and Ci Di due to the soundness of resolution, we will prove that an optimal assignment I of Ci Di is an optimal assignment of φ and falsiﬁes the same number of clauses in Ci Di and φ . We ﬁrst prove that I falsiﬁes the same number of clauses in both multisets: it sufﬁces to prove that I falsiﬁes a clause of the form xi A Di (xi B Di) iff I falsiﬁes A (B), because the rest of clauses in Fi are identical in Di. Assume that I sets xi to true. Then, we have three cases: i) If I falsiﬁes xi B, then I falsiﬁes B because it is a subclause of xi B. ii) If I fasiﬁes B, then I falsiﬁes xi B because we assumed that I sets xi to true. iii) I does not falsify neither xi A nor A. I does not falsify xi A because I sets xi to true. If I falsiﬁes A, then I satisﬁes all the clauses in Di: it satisﬁes every clause of the form xi B because, by the deﬁnition of saturation, B contains a literal whose negation appears in A; and it satisﬁes every clause of the form xi A because I sets xi to true. This is in contradiction with I being optimal because the assignment obtained from I by setting x to false falsiﬁes at least one additional clause (x A in Di). So, I satisﬁes A. The argument above works similarly if we assume that I sets xi to false. I is also an optimal assignment of φ because there exists no assignment I of φ that falsiﬁes more clauses of φ than I does. If so, I could be easily extended to an optimal assignment of φ by setting adequately the truth value of xi due to the fact that no interpretation can falsify simultaneously a clause of the form A and a clause of the form B.

Figure 2 gives the pseudo-code of the new exact inference algorithm for Min SAT proposed in this paper. Given an input multiset of clauses C with n different variables, the algorithm returns the maximum number m of clauses of C that can be falsiﬁed, and an optimal Min SAT assignment I. Functions saturation(C, x) and partition(C, xi) are deﬁned as in the Max SAT case. Function min extension(xi, I, Di) computes a truth assignment for xi as follows: if I falsiﬁes a clause of Di by setting xi

input: C for i := 1 to n C := saturation(C, xi) Ci, Di := partition(C, xi) Fi := {A | x A Di} {B | x B Di} C := Ci Fi endfor m := |C| I := for i := n downto 1 I := I [xi 7 min extension(xi, I, Di)] output: m, I

Figure 2: An exact inference algorithm for Min SAT

to false, then the function returns false; otherwise it returns true. There are two crucial differences with the exact Max SAT algorithm of Section 4: The ﬁrst one is that, after saturating w.r.t. the variable under consideration, the algorithm continues saturating using the multiset Ci Fi instead of the multiset Ci. The second one is the way of computing an optimal assignment.

Theorem 1 Given an input multiset of clauses C with n different variables, the inference algorithm for Min SAT returns the maximum number m of clauses of C that can be falsiﬁed, and an optimal assignment I.

Proof The algorithm constructs a ﬁnite sequence of multisets of clauses φ1 = C1 F1, . . . , φn = Cn Fn from the input multiset C. By Lemma 1, the maximum number of clauses that can be falsiﬁed in each multiset φ1, . . . , φn is the same as in the input multiset C. Since φk contains one less variable than φk 1, for k = 2, . . . , n, we have that φn contains no variables; actually, it only contains empty clauses unless the input multiset is the empty multiset. So, the number of empty clauses in φn is the maximum number of clauses that can be falsiﬁed in φn, and also in φ1, . . . , φn 1 and C. For deriving an optimal assignment we derive a sequence of assignments I1, . . . , In in such a way that (i) Ik is an assignment of the variables xn, xn 1, . . . , xn k+1; and (ii) Ik is derived from Ik 1 by setting Ik(xj) = Ik 1(xj) for j = n, . . . , n k + 2, and Ik(xn k+1) = false if this setting leads Ik to falsify a clause of Dn k+1; otherwise, Ik(xn k+1) = true. We will prove, by induction on k, that Ik is an optimal assignment of Cn k+1 Dn k+1 for k = 1, . . . , n, and in particular that In is an optimal assignment of C1 D1 and, therefore, of the input multiset C. When k = 1, we have that Cn is empty or only contains empty clauses, and Dn is empty or contains unit clauses either of the form xn or of the form xn, but it cannot contain occurrences of both xn and xn. By setting xn in such a way that the clauses in Dn are falsiﬁed, we get an assignment that falsiﬁes the maximum number of clauses in Cn Dn. If Dn is empty, the value of xn is not relevant, and we set xn to true. So, I1 is an optimal assignment of Cn Dn and φn. Assume that Ik is an optimal assignment of Cn k+1 Dn k+1. We must prove that Ik+1 is an optimal assign-

ment of Cn k Dn k. Since Cn k+1 Dn k+1 is a saturation of φn k w.r.t. the variable xn k+1 and the resolution rule is sound, Ik is also an optimal assignment of φn k = Cn k Fn k. Since φn k is obtained from Cn k Dn k by removing the literals containing xn k in Dn k, an assignment cannot falsify more clauses in Cn k Dn k than in φn k. Recall that an assignment cannot simultaneously falsify in Fn k clauses of the form A and B, where A (B) is a clause obtained from a clause of the form xn k A (xn k B) of Dn k. By forcing Ik+1 to set xn k in such a way that the number of clauses falsiﬁed in Dn k is maximized, we have that the number of falsiﬁed clauses in Cn k Dn k and φn k is the same. So, Ik+1 is an optimal assignment of Cn k Dn k.

Example 2 Let φ = {x1, x1 x2, x1 x3, x3} as in Example 1. Resolving the ﬁrst two clauses, we get {x2, x1 x2, x1 x3, x3}. Resolving the second and third clause, we get a saturation of φ w.r.t. x1: {x2, x2 x3, x1 x2 x3, x1 x2 x3, x3}. Hence, C1 = {x2, x2 x3, x3}, D1 = {x1 x2 x3, x1 x2 x3}, and F1 = {x2 x3, x2 x3}. So, the problem reduces to ﬁnd the maximum number of falsiﬁed clauses in C1 F1 = {x2, x2 x3, x2 x3, x2 x3, x3}. We now resolve the second and fourth clause, and get {x2, x3, x2 x3, x3}. We resolve the ﬁrst and third clause, and get a saturation of C1 F1 w.r.t. x2: {x3, x2 x3, x3, x3}. Hence, C2 = {x3, x3, x3}, D2 = {x2 x3}, and F2 = {x3} So, the problem reduces to ﬁnd the maximum number of falsiﬁed clauses in C2 F2 = {x3, x3, x3, x3}. Resolving the two ﬁrst and the two last clauses of {x3, x3, x3, x3}, we get two empty clauses. Hence, C3 = { , }, D3 = {}, and F3 = {}. So, the maximum number of falsiﬁed clauses is 2, and x3 7 true, x2 7 true, x1 7 true is an optimal assignment.

6 Comparing the Inference Schemes for Max SAT and Min SAT A key component of the previous Max SAT and Min SAT algorithms is the concept of saturation, and an essential difference between the two algorithms lies in the way of exploiting its properties. Saturation divides the clauses with occurrences of a variable xi into a group of clauses of the form xi A and another group of clauses of the form xi B, ensuring that every assignment satisﬁes at least all the subclauses A or all the subclauses B due to the fact that, for every pair of clauses (A, B), there is a literal l in A such that l is in B. In the algorithm for Max SAT, by successively computing a saturation w.r.t. all the variables and due to the soundness of the Max SAT resolution rule, we have that the number of clauses that an assignment falsiﬁes in the input multiset C is the same as the number of clauses that it falsiﬁes in Cn Sn i=1 Di, where Cn is either the empty multiset or only contains empty clauses because when Cn is derived all the variables have been eliminated. Since Sn i=1 Di is satisﬁable, it turns out that Cn contains as many empty clauses as the minimum number of clauses that can be falsiﬁed in C, and every assignment satisfying Sn i=1 Di is an optimal Max SAT assignment. Observe that, for ﬁnding a satisfying assignment

of Sn i=1 Di, we just need to set every xi to true (false) if some subclause A (B) is falsiﬁed, because the other group is satisﬁed independently of the value of xi. So, we force the algorithm to satisfy the group of falsiﬁed subclauses to get an optimal Max SAT assignment. We refer the reader to [Bonet et al., 2007] for a formal proof of the previous results. In the algorithm for Min SAT, we exploit the set Di obtained after computing a saturation w.r.t. the variable xi in a different way. Since at most one of the groups of subclauses A and B is falsiﬁed, and Ci contains no occurrences of xi, the Min SAT problem for Ci Di can be safely reduced to the Min SAT problem for Ci Fi. By setting xi to false (true) if there is a subclause A (B) falsiﬁed, we have that every optimal Min SAT assignment of Ci Fi can be extended to an optimal Min SAT assignment of Ci Di. So, we now force the algorithm to falsify, instead of satisfy, the group of falsiﬁed subclauses to get an optimal Min SAT assignment. Observe that reducing a multiset C to Ci Di is stronger than reducing C to Ci Fi because C and Ci Di have the same number of falsiﬁed clauses for each assignment, while C and Ci Fi only preserve the maximum number of falsiﬁed clauses. It can happen, for instance, that C is satisﬁable and Ci Fi is unsatisﬁable as the following example shows: Let C be the satisﬁable multiset {x1 x2, x1 x2, x2 x3}. If we saturate C w.r.t. the variable x1, we have that C1 F1 is the unsatisﬁable multiset {x2, x2, x2 x3}. The SAT Pure Literal Rule (PLR) and Max SAT PLR are identical: If all the occurrences of a propositional variable xi in a multiset have the same polarity, then all the clauses containing the variable xi can be removed. Nevertheless, this rule is not valid in Min SAT as the following counterexample shows: Let C be again the multiset {x1 x2, x1 x2, x2 x3}, which has a maximum of two falsiﬁed clauses by assigning x1, x2 and x3 to false. By applying the previous PLR w.r.t. the variable x1, we derive the multiset {x2 x3}, and by applying the PLR w.r.t. the variable x2, we derive the empty multiset that has no falsiﬁed clauses.

Lemma 2 Let C be a Min SAT instance where all the occurrences of the propositional variable xi have the same polarity, and let C be the Min SAT instance resulting of eliminating all the occurrences of the variable xi in C. Then, C and C have the same maximum number of falsiﬁed clauses.

Proof Since xi occurs only with one polarity, saturating C w.r.t. the variable xi, we get Ci Di = C because in this case Di is formed by all the clauses of C with occurrences of xi, and Ci is formed by the rest of clauses. So, by removing all the occurrences of xi in Di, we get Ci Fi = C . By Lemma 1, C and C have the same maximum number of falsiﬁed clauses.

Therefore, the MINSAT PLR states that if all the occurrences of a propositional variable xi in a Min SAT instance have the same polarity, then all the occurrences of the variable xi can be removed. Figure 3 compares the mean time, in seconds, needed by Min Satz to solve random Min-2SAT instances for different values of the ratio of the number of clauses to the number of variables (r) with a version of Min Satz that applies the Min SAT PLR (W), and a version of Min Satz that does not ap-

Figure 3: Impact on time of the Min SAT PLR

Figure 4: Number of applications of the Min SAT PLR

ply the Min SAT PLR (W/O). A total of 100 instances were solved at each point of the plots. Figure 4 shows the mean number of application of the Min SAT PLR when solving the instances of Figure 3. Figure 5 compares the mean number of nodes (y-axis) of the proof trees derived by Min Satz with and without the application of the Min SAT PLR. In all the ﬁgures the x-axis represents the number of variables. We observe that the application of the Min SAT PLR produces signiﬁcant speed-ups and reductions of the proof tree size on the tested instances, as well as that rule is applied a remarkable number of times. Interestingly, the speed-ups are negligible when the same instances are solved with Max Satz. Even though the worst-case complexity of the exact algorithms for Min SAT and Max SAT coincides, in practice Min SAT may require more inference steps than Max SAT because the number of empty clauses to be derived for a multiset C in Min SAT is always greater than or equal to the number of empty clauses to be derived in Max SAT for C. Moreover, the Min SAT algorithm has to derive resolvents from Ci Fi at each step of the algorithm whereas the Max SAT algorithm

Figure 5: Impact on proof tree size of the Min SAT PLR

only has to derive resolvents from Ci, ignoring Di in the next step. However, this may be an advantage in some cases because the clauses of Di are shortened, and the availability of unit and binary clauses may produce shorter refutations. Many practical optimization problems admit more compact and natural Max SAT and Min SAT encodings if they are encoded using weighted clauses instead of unweighted ones, as well as considering hard and soft clauses. To keep the description as simple as possible, we have presented our results for unweighted Min SAT, but the proposed inference scheme can be extended to both WMin SAT and WPMin SAT. In the case of WMin SAT, we just need to use the weighted version of the resolution rule [Bonet et al., 2007; Larrosa et al., 2008]. From a conceptual point of view, a weighted clause (c, w) is equivalent to have w copies of the unweighted clause c, and the application of the weighted Max SAT resolution rule to two clauses (x D1, w1), (x D2, w2) is equivalent to apply the resolution rule min(w1, w2) times to the unweighted clauses x D1, x D2. So, using the weighted Max SAT resolution rule, φn will be a multiset of weighted empty clauses {( , w1), . . . , ( , wk)}, and w1 + + wk will be the optimal cost of the input multiset. In the case of WPMin SAT, we must ﬁrst derive an equivalent WMin SAT instance as explained below, and then solve the derived instance with the weighted version of our algorithm. We will assume that there is an assignment that satisﬁes all the hard clauses, since otherwise no solution exists. Given a WPMin SAT instance φ whose number of hard clauses is #hard and whose sum of the weights of all its soft clauses is w, we derive a WMin SAT instance φ by adding (i) all the soft clauses in φ, and (ii) the soft clauses (l1, w+1), (l1 l2, w + 1), . . . , (l1 l2 lk, w + 1) for each hard clause hi = l1 l2 lk in φ. These clauses are obtained by negating hi and adding the weight w + 1 to each clause. Observe that an assignment I satisﬁes hi iff I falsiﬁes exactly one clause among l1, l1 l2, . . . , l1 l2 lk; or equivalently, I falsiﬁes hi iff I satisﬁes the clauses l1, l1 l2, . . . , l1 l2 lk. Since the clauses derived from hard clauses have weight w + 1 and we assumed the hard part of

φ is satisﬁable, every optimal solution of φ falsiﬁes exactly one clause derived from a hard clause, and is also an optimal solution of φ. Besides, if the maximum sum of the weights of the falsiﬁed clauses in φ is m, then the maximum sum of the weights of the falsiﬁed clauses in φ is m #hard (w +1). Notice that the way of dealing with hard clauses in Min SAT is different than in Max SAT, where hard clauses are not negated.

7 Conclusions

We described an exact inference algorithm for Min SAT and proved its correctness, extended it to WMin SAT and WPMin SAT, analyzed the differences between the Max SAT and Min SAT inference schemes, and deﬁned and empirically evaluated the Min SAT PLR. All these results are, to the best of our knowledge, the ﬁrst contributions to the study of inference schemes for Min SAT, and provide further evidence that the solving techniques applicable to Max SAT and Min SAT are often different. Hence, we believe that it is important to continue investigating on Min SAT. As future work we plan to empirically compare the inference algorithms for Max SAT and Min SAT, extend them to ﬁnite-domain variables [Ans otegui et al., 2013], and identify optimization problem instances that are particularly wellsuited for Max SAT and Min SAT inference-based methods.

References [Ans otegui et al., 2012] Carlos Ans otegui, Chu Min Li, Felip Many a, and Zhu Zhu. A SAT-based approach to Min SAT. In Proc. of CCIA-2012, pages 185 189, 2012. [Ans otegui et al., 2013] Carlos Ans otegui, Maria Luisa Bonet, Jordi Levy, and Felip Many a. Resolution procedures for multiple-valued optimization. Information Sciences, 227:43 59, 2013. [Argelich et al., 2008] Josep Argelich, Chu Min Li, Felip Many a, and Jordi Planes. The ﬁrst and second Max-SAT evaluations. Journal on Satisﬁability, Boolean Modeling and Computation, 4:251 278, 2008. [Argelich et al., 2011] Josep Argelich, Chu Min Li, Felip Many a, and Jordi Planes. Analyzing the instances of the maxsat evaluation. In Proc. of SAT-2011, pages 360 361, 2011. [Argelich et al., 2012] Josep Argelich, Alba Cabiscol, Inˆes Lynce, and Felip Many a. Efﬁcient encodings from CSP into SAT, and from Max CSP into Max SAT. Multiple Valued Logic and Soft Computing, 19(1-3):3 23, 2012. [Argelich et al., 2013] Josep Argelich, Chu Min Li, Felip Many a, and Zhu Zhu. Min SAT versus Max SAT for optimization problems. In Proc. of CP 2013, pages 133 142, 2013. [Argelich et al., 2014] Josep Argelich, Chu Min Li, Felip Many a, and Zhu Zhu. Many-valued Min SAT solving. In Proc. of ISMVL 2014, pages 32 37, 2014. [Bonet et al., 2006] Mar ıa Luisa Bonet, Jordi Levy, and Felip Many a. A complete calculus for Max-SAT. In Proc. of SAT-2006, pages 240 251, 2006.

[Bonet et al., 2007] Mar ıa Luisa Bonet, Jordi Levy, and Felip Many a. Resolution for Max-SAT. Artiﬁcial Intelligence, 171(8 9):240 251, 2007. [Heras et al., 2012] Federico Heras, Ant onio Morgado, Jordi Planes, and Joao Marques-Silva. Iterative SAT solving for minimum satisﬁability. In Proc. of ICTAI 2012, pages 922 927, 2012. [Ignatiev et al., 2013] Alexey Ignatiev, Ant onio Morgado, Jordi Planes, and Jo ao Marques-Silva. Maximal falsiﬁability - deﬁnitions, algorithms, and applications. In Proc. of LPAR 2013, pages 439 456, 2013. [Ignatiev et al., 2014] Alexey Ignatiev, Ant onio Morgado, and Jo ao Marques-Silva. On reducing maximum independent set to minimum satisﬁability. In Proc. of SAT 2014, pages 103 120, 2014. [Kohli et al., 1994] Rajeev Kohli, Ramesh Krishnamurti, and Prakash Mirchandani. The minimum satisﬁability problem. SIAM J. Discrete Mathematics, 7(2):275 283, 1994. [K ugel, 2012] Adrian K ugel. Natural Max-SAT encoding of Min-SAT. In Proc. of LION 6, 2012. [Larrosa et al., 2008] Javier Larrosa, Federico Heras, and Simon de Givry. A logical approach to efﬁcient Max-SAT solving. Artiﬁcial Intelligence, 172(2 3):204 233, 2008. [Li and Many a, 2009] Chu Min Li and F. Many a. Max SAT, hard and soft constraints. In Armin Biere, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisﬁability, pages 613 631. IOS Press, 2009. [Li et al., 2007] Chu Min Li, Felip Many a, and Jordi Planes. New inference rules for Max-SAT. Journal of Artiﬁcial Intelligence Research, 30:321 359, 2007. [Li et al., 2010a] Chu Min Li, Felip Many a, Nouredine Ould Mohamedou, and Jordi Planes. Resolution-based lower bounds in Max SAT. Constraints, 15(4):456 484, 2010. [Li et al., 2010b] Chu Min Li, Felip Many a, Zhe Quan, and Zhu Zhu. Exact Min SAT solving. In Proc. of SAT-2010, pages 363 368, 2010. [Li et al., 2011] Chu Min Li, Zhu Zhu, Felip Many a, and Laurent Simon. Minimum satisﬁability and its applications. In Proc. of IJCAI-2011, pages 605 610, 2011. [Li et al., 2012] Chu Min Li, Zhu Zhu, Felip Many a, and Laurent Simon. Optimizing with minimum satisﬁability. Artiﬁcial Intelligence, 190:32 44, 2012. [Marathe and Ravi, 1996] M. V. Marathe and S. S. Ravi. On approximation algorithms for the minimum satisﬁability problem. Information Processing Letters, 58:23 29, 1996. [Morgado et al., 2013] Ant onio Morgado, Federico Heras, Mark H. Lifﬁton, Jordi Planes, and Jo ao Marques-Silva. Iterative and core-guided Max SAT solving: A survey and assessment. Constraints, 18(4):478 534, 2013. [Zhu et al., 2012] Zhu Zhu, Chu Min Li, Felip Many a, and Josep Argelich. A new encoding from Min SAT into Max SAT. In Proc. of CP 2012, pages 455 463, 2012.