An Exact Inference Scheme for MinSAT

1 Introduction

MinSAT is the problem of finding an assignment that maximizes the number of falsified clauses (or equivalently, minimizes the number of satisfied clauses) in a multiset of clauses, and MaxSAT is the problem of finding an assignment that minimizes the number of falsified clauses (or equivalently, maximizes the number of satisfied clauses). When weights are added to clauses, we refer to these problems as weighted MaxSAT/MinSAT. When there are clauses considered to be hard and clauses considered to be soft, we refer to them as (weighted) partial MaxSAT/MinSAT.

The development of MaxSAT solvers incorporating novel and powerful solving techniques [Li and Many`a, 2009], as well as the annual celebration of an evaluation of MaxSAT solvers [Argelich et al., 2008], have been decisive to consolidate MaxSAT-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 MaxSAT, a number of researchers have started to look into MinSAT in the last five years. At first sight, one could think that the solving techniques and encodings to be used in MinSAT 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.

Felip Many `a

Artificial Intelligence Research Inst. (IIIA) Spanish National Research Council (CSIC)

ones used in MaxSAT and, therefore, that there is no need of investigating MinSAT 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 profile of MaxSAT and MinSAT 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 findings suggest that it is worth to investigate MinSAT, and find out whether it can be used as a generic problem solving approach for optimization problems either separately or in combination with MaxSAT. It is also worth mentioning that solving MinSAT is meaningful for both satisfiable and unsatisfiable instances, whereas solving MaxSAT is only meaningful for unsatisfiable instances.

Let us mention two examples that illustrate some differences between MaxSAT and MinSAT. The first example is about solvers: In branch-and-bound MinSAT solvers one has to compute, at every node of the search tree, an upper bound on the maximum number of clauses that can be falsified, and in branch-and-bound MaxSAT solvers one has to compute a lower bound on the minimum number of clauses that can be falsified. 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 MinSAT greatly outperforms MaxSAT on combinatorial auctions and MaxClique instances using solvers sharing many implementation details like MinSatz [Li et al., 2012] and MaxSatz [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 satisfied with both MaxSAT and MinSAT encodings. Using the MaxSAT direct encoding [Argelich et al., 2012], we must add one clause for every no-good, while using the MinSAT 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 MinSAT, and a quadratic number of clauses in MaxSAT. We are in the opposite situation if we want to represent the constraint X ̸= Y , So, it seems that MaxSAT and MinSAT could be complementary in some scenarios [Argelich et al., 2013].

In this paper we focus on inference schemes for MaxSAT and MinSAT, and present original contributions to MinSAT. There exists a MaxSAT resolution rule (c.f. Section 4) that can also be applied to MinSAT because it preserves the number of falsified clauses when the premises of the rule are replaced by its conclusions. Besides, there exists also an exact inference algorithm for MaxSAT [Bonet et al., 2007] that derives, by applying the MaxSAT resolution rule a finite number of times following a certain strategy, as many empty clauses as the minimum number of clauses that can be falsified in a multiset of clauses. Nevertheless, it is an open problem to figure out how an inference rule may be used to compute a MinSAT solution; i.e., to derive as many empty clauses as the maximum number of clauses that can be falsified.

The main objective of this work is to solve that open problem by devising an exact inference algorithm for MinSAT that relies on the existing inference algorithm for MaxSAT but contains significant differences despite of the fact that both algorithms apply the MaxSAT resolution rule. In particular, we describe the algorithm and prove its correctness, show how it can be extended to deal with weighted MinSAT and weighted partial MinSAT instances, analyze the differences between the MaxSAT and MinSAT inference schemes, and define and empirically evaluate the MinSAT Pure Literal Rule.

The paper is organized as follows: Section 2 gives basic definitions. Section 3 summarizes the related work. Section 4 presents the existing inference scheme for MaxSAT. Section 5 describes the inference algorithm for MinSAT, and proves its correctness. Section 6 compares the MaxSAT and MinSAT inference schemes, and presents new insights into MinSAT. 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 infinity. A clause is hard if its weight is infinity; otherwise it is soft. A weighted partial MinSAT (MaxSAT) instance is a multiset of weighted clauses φ = {(h1,∞), . . . , (hk,∞), (c1, w1), . . . , (cm, wm)}, where the first k clauses are hard and the last m clauses are soft. For simplicity, in what follows, we omit infinity 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 MinSAT (MaxSAT), or WPMinSAT (WPMaxSAT), for an instance φ is the problem of finding an assignment in which the sum of the weights of the satisfied (falsified) soft clauses is minimal, and all the hard clauses are satisfied. The Weighted MinSAT (MaxSAT) problem, or WMinSAT (WMaxSAT), is the WPMinSAT (WPMaxSAT) problem when there are no hard clauses. The Partial MinSAT (MaxSAT) problem, or PMinSAT (PMaxSAT), is the WPMinSAT (WPMaxSAT) problem when all the soft clauses have the same weight. The (Unweighted) MinSAT (MaxSAT) problem is the Partial MinSAT (MaxSAT) problem when there are no hard clauses.

3 RelatedWork

The work on MinSAT 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 MinSAT started to be studied from a problem solving perspective. The main results of this recent work on MinSAT may be succinctly summarized as follows:

I)Definition of transformation between MinSAT and MaxSAT: Reductions from MinSAT to PMaxSAT were defined in [Li et al., 2010b], but they do not generalize to WPMinSAT. This drawback was overcome with the definition of the natural encoding [K¨ugel, 2012], which was improved in [Zhu et al., 2012]. Reductions of WPMinSAT to Group MaxSAT were evaluated in [Heras et al., 2012].

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

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

IV) Definition and evaluation of genuine MinSAT encodings of relevant problems such as weighted MaxCSP [Argelich et al., 2013; 2014], and graph problems [Ignatiev et al., 2014; 2013].

4 Inference inMaxSAT

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 MaxSAT. It works by adding the conclusion of the rule to the premises, and this may increase the number of falsified clauses in the derived instance. In contrast, the MaxSAT resolution rule works by replacing the premises by its conclusions in such a way that the number of falsified clauses is preserved for every assignment.

The MaxSAT resolution rule is defined as follows [Bonet et al., 2007; Larrosa et al., 2008]:

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 ↦→max extension(xi, I,Di)] output: m, I

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 MaxSAT resolution rule is sound and complete. It is sound because the number of clauses that every assignment falsifies in the premises is the same as the number of clauses that it falsifies in the conclusions. It is complete because, for every multiset of clauses C whose minimum number of falsified clauses is m, the application of the rule (finitely many times) following a strategy explained below derives a multiset formed by exactly m empty clauses.

Before describing the exact inference algorithm for MaxSAT of [Bonet et al., 2007], we need two definitions:

Definition 1 We write C ⊢ D when the multiset of clauses D can be obtained from the multiset C by applying the MaxSAT resolution rule a finite number of times. We write C ⊢x D when this sequence of applications only cuts the variable x.

Definition 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 MaxSAT 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 finitely many times.

Trivially, by the previous definition, 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 first 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: themultiset {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 MaxSAT. 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 falsified, and an optimal MaxSAT 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 satisfies 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 satisfied or all the clauses of the form xi ∨B are satisfied. In this case, xi is set in such a way that all the clauses in Di become satisfied.

The algorithm has two parts. In the first 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 falsified 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 first 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 first 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 falsified clauses is 1, and x3 ↦→ false, x2 ↦→ false, x1 ↦→ true is an optimal assignment.

5 Inference inMinSAT

The goal of an exact MinSAT algorithm is to compute an assignment that falsifies the maximum number of clauses in a MinSAT instance.

In this section we define an algorithm that derives, by applying the MaxSAT resolution rule, as many empty clauses as the maximum number of clauses that can be falsified. First of all, we should note that the MaxSAT resolution rule is also a sound inference rule for MinSAT because its application preserves the number of falsified 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 MinSAT 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 falsifies in φ and in the computed saturation is the same. We then partition the saturation into two multisets as in MaxSAT: 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 MaxSAT where a saturation of Ci w.r.t. xi+1 is computed, we now compute a saturation of the MinSAT 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 MinSAT problem for φ can be reduced to the MinSAT problem for φ′ = Ci ∪ Fi.

Lemma 1 Let φ be a MinSAT instance, and let φ′ be a MinSAT instance derived from φ by first 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 falsifies the same number of clauses in φ and φ′ .

Proof Since every assignment falsifies 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 falsifies the same number of clauses in Ci ∪Di and φ′ . We first prove that I falsifies the same number of clauses in both multisets: it suffices to prove that I falsifies a clause of the form xi ∨ A ∈ Di (xi ∨ B ∈ Di) iff I falsifies 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 falsifies ¯xi ∨B, then I falsifies B because it is a subclause of ¯xi ∨B.

ii) If I fasifies B, then I falsifies ¯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 falsifies A, then I satisfies all the clauses in Di: it satisfies every clause of the form ¯xi ∨ B because, by the definition of saturation, B contains a literal whose negation appears in A; and it satisfies 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 falsifies at least one additional clause (x ∨ A in Di). So, I satisfies 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 falsifies 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 MinSAT 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 falsified, and an optimal MinSAT assignment I.

Functions saturation(C, x) and partition(C, xi) are defined as in the MaxSAT case. Function min extension(xi, I,Di) computes a truth assignment for xi as follows: if I falsifies 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 ↦→min extension(xi, I,Di)] output: m, I

to false, then the function returns false; otherwise it returns true.

There are two crucial differences with the exact MaxSAT algorithm of Section 4: The first 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 MinSAT returns the maximum number m of clauses of C that can be falsified, and an optimal assignment I.

Proof The algorithmconstructs a finite sequence ofmultisets of clauses φ1 = C1 ∪ F1, . . . , φn = Cn ∪ Fn from the input multiset C. By Lemma 1, the maximum number of clauses that can be falsified 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 falsified 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 falsified, we get an assignment that falsifies 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 assignment 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 falsified in Dn-k is maximized, we have that the number of falsified 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 first 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 find the maximum number of falsified 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 first 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 find the maximum number of falsified clauses in C2 ∪ F2 = {x3, x3, x3, x3}.

Resolving the two first 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 falsified clauses is 2, and x3 ↦→ true, x2 ↦→ true, x1 ↦→ true is an optimal assignment.

6 Comparing the Inference Schemes for MaxSAT and MinSAT

A key component of the previous MaxSAT and MinSAT 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 satisfies 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 MaxSAT, by successively computing a saturation w.r.t. all the variables and due to the soundness of the MaxSAT resolution rule, we have that the number of clauses that an assignment falsifies in the input multiset C is the same as the number of clauses that it falsifies in Cn ∪ ⋃ni=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 ⋃ni=1 Di is satisfiable, it turns out that Cn contains as many empty clauses as the minimum number of clauses that can be falsified in C, and every assignment satisfying ⋃ni=1 Di is an optimal MaxSAT assignment. Observe that, for finding a satisfying assignment of ⋃ni=1 Di, we just need to set every xi to true (false) if some subclause A (B) is falsified, because the other group is satisfied independently of the value of xi. So, we force the algorithm to satisfy the group of falsified subclauses to get an optimal MaxSAT assignment. We refer the reader to [Bonet et al., 2007] for a formal proof of the previous results.

In the algorithm for MinSAT, 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 falsified, and Ci contains no occurrences of xi, the MinSAT problem for Ci ∪Di can be safely reduced to the MinSAT problem for Ci ∪ Fi. By setting xi to false (true) if there is a subclause A (B) falsified, we have that every optimal MinSAT assignment of Ci ∪ Fi can be extended to an optimal MinSAT assignment of Ci∪Di. So, we now force the algorithm to falsify, instead of satisfy, the group of falsified subclauses to get an optimal MinSAT 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 falsified clauses for each assignment, while C and Ci∪Fi only preserve the maximum number of falsified clauses. It can happen, for instance, that C is satisfiable and Ci ∪ Fi is unsatisfiable as the following example shows: Let C be the satisfiable multiset {x1 ∨ x2, x1 ∨ x2, x2 ∨ x3}. If we saturate C w.r.t. the variable x1, we have that C1 ∪ F1 is the unsatisfiable multiset {x2, x2, x2 ∨ x3}.

The SAT Pure Literal Rule (PLR) and MaxSAT 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 MinSAT as the following counterexample shows: Let C be again the multiset {x1∨x2, x1∨x2, x2∨x3}, which has a maximum of two falsified 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 falsified clauses.

Lemma 2 Let C be a MinSAT instance where all the occurrences of the propositional variable xi have the same polarity, and let C ′ be the MinSAT instance resulting of eliminating all the occurrences of the variable xi in C. Then, C and C ′ have the same maximum number of falsified 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 falsified clauses. □

Therefore, the MINSAT PLR states that if all the occurrences of a propositional variable xi in a MinSAT 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 MinSatz 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 MinSatz that applies the MinSAT PLR (W), and a version of MinSatz that does not apply the MinSAT 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 MinSAT PLR when solving the instances of Figure 3. Figure 5 compares the mean number of nodes (y-axis) of the proof trees derived by MinSatz with and without the application of the MinSAT PLR. In all the figures the x-axis represents the number of variables.

We observe that the application of the MinSAT PLR produces significant 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 MaxSatz.

Even though the worst-case complexity of the exact algorithms for MinSAT and MaxSAT coincides, in practice MinSAT may require more inference steps than MaxSAT because the number of empty clauses to be derived for a multiset C in MinSAT is always greater than or equal to the number of empty clauses to be derived in MaxSAT for C. Moreover, the MinSAT algorithm has to derive resolvents from Ci ∪ Fi at each step of the algorithm whereas the MaxSAT algorithm only has to derive resolvents fromCi, 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.

Figure 5: Impact on proof tree size of the MinSAT PLR

Many practical optimization problems admit more compact and natural MaxSAT and MinSAT 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 MinSAT, but the proposed inference scheme can be extended to both WMinSAT and WPMinSAT.

In the case of WMinSAT, 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 MaxSAT 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 MaxSAT 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 WPMinSAT, we must first derive an equivalent WMinSAT 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 satisfies all the hard clauses, since otherwise no solution exists.

Given a WPMinSAT instance φ whose number of hard clauses is #hard and whose sum of the weights of all its soft clauses is w, we derive a WMinSAT 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 satisfies hi iff I falsifies exactly one clause among l1, l1 ∨ l2, . . . , l1 ∨ l2 ∨ · · · ∨ lk; or equivalently, I falsifies hi iff I satisfies 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 satisfiable, every optimal solution of φ′ falsifies 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 falsified clauses in φ′ is m, then the maximum sum of the weights of the falsified clauses in φ is m-#hard×(w+1). Notice that the way of dealing with hard clauses in MinSAT is different than in MaxSAT, where hard clauses are not negated.

7 Conclusions

We described an exact inference algorithm for MinSAT and proved its correctness, extended it to WMinSAT and WPMinSAT, analyzed the differences between the MaxSAT and MinSAT inference schemes, and defined and empirically evaluated the MinSAT PLR. All these results are, to the best of our knowledge, the first contributions to the study of inference schemes for MinSAT, and provide further evidence that the solving techniques applicable to MaxSAT and MinSAT are often different. Hence, we believe that it is important to continue investigating on MinSAT.

As future work we plan to empirically compare the inference algorithms for MaxSAT and MinSAT, extend them to finite-domain variables [Ans´otegui et al., 2013], and identify optimization problem instances that are particularly wellsuited for MaxSAT and MinSAT inference-based methods.