A Clause Tableau Calculus for MaxSAT

1 Introduction

There has been tremendous progress in theoretical and applied aspects of the MaxSAT problem over the last decade. As a result, there are now a number of competitive solvers that are able to solve challenging optimization problems in different areas (see e.g. [Abram´e and Habet, 2015; Ans´otegui et al., 2013; 2016a; 2016b; Li and Many`a, 2009; Martins et al., 2014; Morgado et al., 2013; Narodytska and Bacchus, 2014] and the references therein for previous and related work).

One lesson learned during that time is that the inference rules applied in SAT solving usually cannot be applied in MaxSAT, because such rules preserve satisfiability but do not preserve the number of falsified clauses. This implies that successful SAT solving techniques such as unit propagation are unsound in MaxSAT.

The most relevant studies conducted to date about inference rules in MaxSAT analyze how an extended resolution rule, or refinements of this rule, can be applied to solve MaxSAT [Abram´e and Habet, 2014a; Bonet et al., 2007; Heras and Larrosa, 2006; Larrosa et al., 2008; Li et al., 2007].

MaxSAT resolution replaces two parent clauses (x _ a1 _ ▷ ▷ ▷ _ as and x _ b1 _ ▷ ▷ ▷ _ bt) with their resolvent (a1 _ ▷ ▷ ▷ _ as _ b1 _ ▷ ▷ ▷ _ bt) plus s + t compensation clauses that are not needed in SAT (x _ a1 _ ▷ ▷ ▷ _ as _ b1↪ ▷ ▷ ▷ ↪ x _ a1 _ ▷ ▷ ▷ _ as _ b1 _ ▷ ▷ ▷ _ bt-1 _ bt↪ x _ b1 _ ▷ ▷ ▷ _ bt _ a1↪ ▷ ▷ ▷ ↪ x _ b1 _ ▷ ▷ ▷ _ bt _ a1 _ ▷ ▷ ▷ _ as-1 _ as). Compensation clauses FelipMany`a and Joan Ramon Soler Artificial Intelligence Research Inst. (IIIA) Spanish National Research Council (CSIC)

⇤Research partially supported by the National Natural Science Foundation of China (Grant no. 61472147), the Generalitat de Catalunya grant AGAUR 2014-SGR-118, and the Ministerio de Econom´ıa y Competividad project RASO TIN2015-71799-C2-1-P. The second author was supported by Mobility Grant PRX16/00215 of the Ministerio de Educaci ´on, Cultura y Deporte.

ensure that the number of falsified clauses is preserved but complicate the application of the rule. A nice feature of MaxSAT resolution is its completeness [Bonet et al., 2006; 2007]: given a multiset of clauses whose minimum number of falsified clauses is m, the application of MaxSAT resolution, finitely many times and following a certain strategy, derives a multiset formed by exactly m empty clauses.

The present paper investigates how to extend the clause tableau method for SAT [D'Agostino, 1999; H¨ahnle, 2001] to solve MaxSAT. The contributions of our work can be summarized as follows:

• ÷ A clause tableau calculus for MaxSAT that is sound and complete in the following sense: the minimum number of clauses that can be falsified in a multiset of clauses φ is m iff the minimum number of empty clauses, among the branches of a clause tableau for φ, that can be derived by applying the tableau rules of the calculus until saturation is m. 1
• ÷ A tableau-based MaxSAT algorithm that computes both the minimum number of clauses that can be falsified in φ, and an optimal assignment.
• ÷ Description of how the algorithm can be extended to solve weighted MaxSAT and weighted partial MaxSAT.

It is the first time, to the best of our knowledge, that a tableau calculus has been employed in combinatorial optimization and, in particular, to solve Boolean optimization problems. Moreover, the proposed calculus offers an inference system that is simpler and more intuitive than MaxSAT resolution: no compensation clauses are needed, and all the derived clauses are either empty or unit.

An advantage of the tableau method for SAT is that it can deal directly with formulas that are not in conjunctive normal form (CNF). Tableaux do not need to apply CNF conversion, avoiding so the space complexity of some conversion CNF algorithms. It remains an open question how to extend the contributions of the present paper to solve MaxSAT for nonCNF formulas.

The paper is organized as follows: Section 2 gives basic concepts about SAT and MaxSAT. Section 3 describes how clause tableaux can be used to solve SAT. Section 4 defines an original clause tableau calculus for MaxSAT, proves its soundness and completeness, and describes an exact MaxSAT algorithm. Section 5 shows how the proposed algorithm can be extended to solve weighted MaxSAT and weighted partial MaxSAT. Section 6 contains the concluding remarks, and points out future research directions.

1 By saturation we mean that all the possible applications of inference rules were performed.

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 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 MaxSAT instance is a multiset of weighted clauses φ = ¶(h1↪1)↪ ▷ ▷ ▷ ↪ (hk↪1)↪ (c1↪w1)↪ ▷ ▷ ▷ ↪ (cm↪ wm)♦, where the first k clauses are hard and the last m clauses are soft. The total number of weighted clauses in φ is denoted by ♣φ♣. For simplicity, in what follows, we omit infinity weights, and write φ = ¶h1↪ ▷ ▷ ▷ ↪ hk↪ (c1↪ w1)↪ ▷ ▷ ▷ ↪ (cm↪ wm)♦. A soft clause (c↪w) is equivalent to having w copies of the clause (c↪ 1), and ¶(c↪ w1)↪ (c↪ w2)♦ is equivalent to (c↪ w1 + w2).

A truth assignment assigns to each propositional variable either 0 (false) or 1 (true). Weighted Partial MaxSAT, or WPMaxSAT, for an instance φ is the problem of finding an assignment that satisfies all the hard clauses and minimizes the sum of the weights of the falsified soft clauses; such an assignment is called optimal assignment. The Weighted MaxSAT problem, or WMaxSAT, is WPMaxSAT when there are no hard clauses. The Partial MaxSAT problem, or PMaxSAT, is WPMaxSAT when all the soft clauses have the same weight. The (Unweighted) MaxSAT problem is PMaxSAT when there are no hard clauses. The SAT problem, or SAT, is PMaxSAT when there are no soft clauses.

3 Clause Tableaux for SAT

It is common to view the tableau method for solving SAT as a proof by case distinction that allows one to systematically generate subcases until elementary contradictions are reached. In the context of SAT, a clause tableau is a tree with a finite number of branches whose nodes are labelled with clauses, and a branch is a maximal path in a tree with a finite number of nodes. A branch is closed if there are two nodes labelled with complementary unit clauses; otherwise, it is open. A clause tableau is closed iff all its branches are closed.

Given a set of clauses C = ¶C1↪ ▷ ▷ ▷ ↪Cm♦, we create an initial tableau that has a single branch with m nodes, where each node is labelled with a clause of C. Then, we select an open branch B and a non-unit clause l1 _ ▷ ▷ ▷ _ lr of C that has not yet been expanded in B, and append r nodes below B, labelling each node with a different unit clause from ¶l1↪ ▷ ▷ ▷ ↪ lr♦. This process of creating r new branches from B is known as the application of the extension rule. If there are two complementary unit clauses in a branch, we close it. This process continues until either all the branches are closed, or the application of the extension rule on a branch until saturation leaves it open. C is declared to be unsatisfiable in the first case, and satisfiable in the second case.

Example 1 To determine the satisfiability of C = ¶x1↪ x1 _ x2↪ x1 _ x2♦ with clause tableaux we start by creating the initial tableau (T0):

x1 _ x2

We then expand the second node, and close he leftmost branch (it has the occurrence of both x1 and x1, and the closing is denoted by ⇥ in the tableau), obtaining the following clause tableau (T1):

⇥

Finally, we expand the third node on the rightmost branch, and get a closed tableau (T2) that provides a clause tableau proof of the unsatisfiability of C:

x1

⇥

⇥

Formally, a clause tableau proof of the unsatisfiability of a set of clauses φ is a sequence of clause tableaux T0↪ ▷ ▷ ▷ ↪ Tn such that T0 is an initial tableau, Tn is a closed tableau, and Ti has been obtained by a single application of the extension rule on an open branch of Ti-1 for i = 1↪ ▷ ▷ ▷ ↪ n. In a proof of satisfiability, Tn must have some open branch after applying the extension rule on it until saturation. Besides, the literals occurring in the unit clauses of the open branch provide a satisfying assignment of φ.

It is common to say that Tn is a clause tableau proof because it collapses all the sequence of tableaux. In Example 1, T0↪ T1↪ T2 is a clause tableau proof, although T2 alone is also considered to be a clause tableau proof.

From a semantic perspective, given a set of clauses φ and a clause tableau T for φ, we have that φ is satisfiable iff there is a branch in T such that the conjunction of all its clauses is satisfiable (or alternatively, φ is unsatisfiable iff all the branches of T are unsatisfiable).

4 Clause Tableaux for MaxSAT

The tableau method for SAT is not valid for solving MaxSAT, among other reasons, because it stops the search in a branch once a contradiction is detected. Moreover, in the case of MaxSAT, we should pay attention to not use the same literal to detect different contradictions; for example, an exact MaxSAT method detects one contradiction in ¶x1↪ x1↪ x1♦, whereas it detects two contradictions in ¶x1↪ x1↪ x1↪ x1♦ because x1 can be used only once in the first case.

We define below a tableau method for MaxSAT that contemplates to find more than one contradiction in each branch, and that marks as used both the clauses that have already been expanded and the complementary unit clauses involved in a contradiction; in this way, the tableau method avoids to use more than once the same clause in a branch. Recall that we are now working with multisets of clauses. In the rest of the paper, unless otherwise stated, when we say clause tableau we mean clause tableau for MaxSAT.

Definition 1 A clause tableau is a tree with a finite number of branches whose nodes are labelled with clauses that are declared to be either marked or unmarked in each branch. A branch is a maximal path in a tree, and we assume that branches have a finite number of nodes.

Definition 2 Let φ = ¶C1↪ ▷ ▷ ▷ ↪ Cm♦ be a multiset of clauses. A clause tableau for φ is constructed by a sequence of applications of the following rules:

• Initialize A tree with a single branch with m nodes such that each node is labelled with a clause of φ is a clause tableau for φ. Such a tableau is called initial tableau and its clauses are declared to be unmarked.
• Extension Given a clause tableau T for φ, a branch B of T , and a node of B labelled with an unmarked non-unit clause l1 _ · · · _ lr, the tableau obtained by appending r nodes below B, labelling each node with a different unit clause from ¶l1↪ ▷ ▷ ▷ ↪ lr♦, is a clause tableau for φ. The clause l1 _ · · · _ lr is declared to be marked in the newly created branches, and the unit clause li, for i = 1↪ ▷ ▷ ▷ ↪ r, is declared to be unmarked in the newly created branch in which it occurs.
• Contradiction Given a clause tableau T for φ, a branch B of T, and two nodes of B labelled with two unmarked unit clauses l and l, the tableau obtained by appending a node labelled with an empty clause below B is a clause tableau for φ. The empty clause is declared to be unmarked in the newly created branch, and the complementary unit clauses, l and l, are declared to be marked.

Definition 3 Let T be a clause tableau for a multiset of clauses φ, and let B be a branch of T. The branch B is saturated when all its unmarked clauses are empty and unit clauses, and the contradiction rule cannot be further applied on B. The tableau T is saturated iff all its branches are saturated. The cost of a saturated branch is the number of empty clauses in it. The cost of a saturated tableau is the minimum cost among all its branches.

The notion of saturation is crucial in MaxSAT because it indicates that the application of inference rules has been completed. As we show below, the minimum number of clauses that can be falsified in a multiset of clauses φ is k iff the cost of a saturated tableau for φ is k. So, the systematic construction of a saturated clause tableau for φ provides an exact method for MaxSAT, and each saturated tableau is a proof.

⇤

⇤

Figure 1: A saturated clause tableau for φ = ¶x1↪ x2↪ x3↪ x1_ x2↪ x1 _ x3↪ x2 _ x3♦ that proves that the minimum number of falsified clauses in φ is 2.

Example 2 Let φ be the multiset of clauses ¶x1↪ x2↪ x3↪ x1 _ x2↪ x1 _ x3↪ x2 _ x3♦. Figure 1 shows a saturated clause tableau T for φ, and Figure 2 shows the steps performed for saturating the leftmost branch of T .

In Figure 2, we first create an initial tableau. Secondly, we apply the extension rule to clause x1 _ x2, and mark it in the newly created branches (in the figure we write in bold the marked clauses in the leftmost branch, which is the branch on which we concentrate in this example). Thirdly, we apply the contradiction rule to x1 and x1, and mark these clauses in the leftmost branch. Fourthly, we apply the extension rule to x1 _ x3, and mark the clause in the newly created branches. Fifthly, we apply the extension rule to x2 _ x3, and mark the clause in the newly created branches. Sixthly, we apply the contradiction rule to x2 and x2, and mark these clauses in the leftmost branch. No more inference rules can be applied on the leftmost branch and therefore the branch is saturated, having as unmarked clauses ¶⇤↪⇤↪ x1↪ x3♦. A similar process is repeated to create the rest of branches in Figure 1.

The saturated branches of the tableau of Figure 1 have cost 2 except for branches 3 and 6 (counting from left to right) that have cost 3. The unmarked clauses in each branch are: ¶⇤↪⇤↪ x1↪ x3♦ (branch 1), ¶⇤↪⇤↪ x1↪ x2♦ (branch 2), ¶⇤↪⇤↪⇤♦ (branch 3), ¶⇤↪⇤↪ x2↪ x3♦ (branch 4), ¶⇤↪ ⇤↪ x2↪ x3♦ (branch 5), ¶⇤↪ ⇤↪ ⇤♦ (branch 6), ¶⇤↪⇤↪ x1↪ x2♦ (branch 7), and ¶⇤↪⇤↪ x1↪ x3♦ (branch 8). Therefore, the minimum number of falsified clauses in φ is 2.

Lemma 1 There exists a saturated tableau for each multiset of clauses φ.

Proof We prove the lemma by induction on the number m of clauses in φ = ¶C1↪ ▷ ▷ ▷ ↪ Cm♦.

Basis: for m = 1, it is trivial. If the unique clause in φ has more than one literal, we apply the extension rule on the single branch of the initial tableau and get a saturated tableau; otherwise, the initial tableau is already saturated.

Inductive step: assume that T is a saturated tableau for ¶C1↪ ▷ ▷ ▷ ↪Ck-1♦. We prove that there exists a saturated tableau T 00 for ¶C1↪ ▷ ▷ ▷ ↪Ck♦: Let T 0 be the tableau obtained from T by expanding Ck in each branch of T , and let T 00 be the tableau obtained from T 0 by applying the contradiction rule on each branch of T 0 . The extension and the contradiction rule can be applied at most once in each branch, and T 00 is saturated because no tableau rules can be applied on the branches of T 00 . ⇤

4.1 Soundness and Completeness

We now prove that the minimum number of clauses that can be falsified in a multiset of clauses φ is m iff the cost of each saturated tableau for φ is m.

Theorem 1 Soundness. Let φ be a multiset of clauses, and let T be a saturated clause tableau for φ of cost m. Then, the minimum number of clauses that can be falsified in φ is m.

Proof T was obtained by creating a sequence of clause tableaux T0↪ ▷ ▷ ▷ ↪ Tn (n ≥ 0) such that T0 is an initial tableau for φ, Tn = T , and Ti was obtained by a single application of the extension or the contradiction rule on an branch of Ti-1 for i = 1↪ ▷ ▷ ▷ ↪ n. Assume that I is an optimal assignment of φ that falsifies k clauses, where k 6= m. By induction on n, we prove that the minimum number of unmarked clauses that I falsifies among the branches of T0↪ ▷ ▷ ▷ ↪ Tn (and in particular of T) is k:

Basis: T0 has a single branch whose nodes are labelled with the clauses of φ, and such clauses are declared to be unmarked in that branch. So, I falsifies k unmarked clauses in T0, and k is the minimum number of unmarked clauses that can be falsified in T0.

Inductive step: Assume that the minimum number of unmarked clauses that I falsifies among the branches of Ti-1 is k. We prove that the minimum number of unmarked clauses that I falsifies among the branches of Ti is also k.

Since Ti was constructed from Ti-1 by applying either the contradiction rule or the extension rule on a branch B of Ti-1 and the rest of branches of Ti-1 remain unchanged in Ti, we just need to prove that I satisfies the same number of unmarked clauses in B and in at least one of the newly created branches, and does not decrease that number in the rest of newly created branches. We distinguish two cases:

• ÷ The contradiction rule was applied on B: two complementary unit clauses in B become marked and an empty clause is added in the new branch B0 . Since exactly one

• of the newly marked unit clauses was falsified by I and we added one empty clause, I falsifies the same number of unmarked clauses in B and B0 .
• ÷ The extension rule was applied on B: If I satisfies the extended clause C of B, then I satisfies the leaf node of at least one of the newly created branches, say B0 . The number of falsified unmarked clauses is preserved in B0 and does not decrease in the rest of branches. If I falsifies C, then I falsifies the leaf nodes of all the newly created branches, and the number of falsified unmarked clauses is preserved in all these branches because C becomes marked after the extension.

We proved that the minimum number of unmarked clauses that I falsifies among the branches of T0↪ ▷ ▷ ▷ ↪ Tn -and in particular of T- is k but this is in contradiction with T being a saturated tableau for φ that has cost m: Since T is saturated, the unmarked clauses of any branch B of T with minimum cost is the union of a multiset with m empty clauses and a multiset of unit clauses whose complementary unit clauses do not occur in it. The multiset of unit clauses is clearly satisfiable, and so the minimum number of unmarked clauses that can be falsified in B is m (not k), and is at least m in the rest of branches of T. Hence, the minimum number of clauses that can be falsified in φ is m.

⇤

Theorem 2 Completeness. Let φ be a multiset of clauses whose minimum number of clauses that can be falsified is m. Then, each saturated clause tableau T for φ has cost m.

Proof Assume that there is a saturated tableau T for φ that does not have cost m. We distinguish two cases:

(i) T has a branch B that has cost k, where k < m. Then, the unmarked clauses of B are the union of a multiset with k empty clauses and a satisfiable multiset of unit clauses (otherwise, B could not be saturated because the contradiction rule could be applied). We define an assignment I of φ as follows: I(x) = 1 (I(x) = 0) if x (x) is an unmarked clause of B, and I(x0 ) = 0 if variable x0 does not occur in any unmarked clause of B. We next prove that I satisfies at least ♣φ♣ - k clauses of φ, or equivalently I falsifies at most k clauses of φ. I is clearly an optimal assignment of B. If we undo all the applications of the contradiction rule in B, we get a branch B0 whose unmarked clauses form a multiset of unit clauses φ0 that contains as many unit clauses as clauses are in φ, and each literal of each unit clause of φ0 was derived from a different clause of φ. Since the clause of φ0 are unit and there are k complementary pairs of unit clauses, I satisfies ♣φ♣-k clauses of φ0 , and at least ♣φ♣ - k clauses of φ. We have therefore an assignment of φ that cannot falsify more than k clauses, but this is in contradiction with m being the minimum number of clauses that can be falsified in φ because k < m.

(ii) T has no branch of cost m. This is in contradiction with m being the minimum number of clauses that can be falsified in φ. Since the tableau rules preserve the minimum number of falsified clauses, T must have a saturated branch of cost m.

Hence, each saturated clause tableau T for a multiset of clauses φ has cost m if the minimum number of clauses that can be falsified in φ is m. ⇤

input: a multiset of clauses φ over the set of propositional variables ¶x1↪ ▷ ▷ ▷ ↪ xn♦ T := initial clause tableau for φ min cost := number of clauses in φ while 9 an unmarked non-unit clause C in a branch B of T do T := T after applying the extension rule to C on B Let B1↪ ▷ ▷ ▷ ↪ Br be the newly created branches Declare C to be marked in B1↪ ▷ ▷ ▷ ↪ Br T := T after applying the contradiction rule on B1↪ ▷ ▷ ▷ ↪ Br if 9 saturated branch Bi 2 T & min cost > #empty(Bi) thenmin cost := #empty(Bi) endwhile B := branch of T of minimum cost (min cost) I := ; for i := 1 to n if xi is an unmarked unit clause in B then I := I [ ¶xi 1♦ else I := I [ ¶xi 0♦ endfor output: min cost, I

4.2 A Tableau-Based Algorithm for MaxSAT

Figure 3 shows the pseudo-code of an algorithm for MaxSAT that creates a saturated tableau for the input multiset of clauses φ. In addition, it generates an optimal assignment for φ. Function #empty returns the number of empty clauses in the branch provided as parameter.

The algorithm produces an optimal assignment I of the input multiset of clauses φ from a branch B of minimum cost of the saturated tableau created in the first part of the algorithm. The optimal assignment I sets a variable x to 1 (0) if B has a node labelled with the unmarked clause x (x); the rest of variables can be set to either 0 or 1, but we set them to 0 in the algorithm.

The argument to show that I is optimal comes from the proof of Theorem 2: Let m be the value of min cost returned by the algorithm. It is clear that I is an optimal assignment of B. If we undo all the applications of the contradiction rule in B, we get a branch B0 whose unmarked clauses form a multiset of unit clauses φ0 that contains as many unit clauses as clauses are in φ, and each literal of each unit clause of φ0 was derived from a different clause of φ. Since the clause of φ0 are unit and there are m complementary pairs of unit clauses, I satisfies ♣φ♣ -m clauses of φ0 , and at least ♣φ♣ - m clauses of φ. Since B is a branch of minimum cost of a saturated tableau for φ and B has cost m, each assignment of φ falsifies at least m clauses. Therefore, I satisfies exactly ♣φ♣ - m clauses of φ and is optimal.

Note that the saturated branches that do not have minimum cost only contain three empty clauses. This means

Example 3 Let φ be the multiset from Example 4. From each saturated branch of minimum cost in the tableau of Figure 1 we derive an optimal assignment. For example, from branch 1, whose unmarked clauses are ¶⇤↪ ⇤↪ x1↪ x3♦, we derive the assignment ¶x1 1↪ x2 0↪ x3 0♦. By convention, we set the literals that do not appear in unmarked clauses to 0, but they could also be set to 1. Hence, ¶x1 1↪ x2 1↪ x3 0♦ is also an optimal assignment.

that the assignments ¶x1 0↪ x2 0↪ x3 0♦ and ¶x1 1↪ x2 1↪ x3 1♦ are not optimal.

An immediate application of our tableau calculus is to replace the common branching in branch-and-bound (BnB) MaxSAT solvers such as [Abram´e and Habet, 2014b; Argelich and Many`a, 2006; Alsinet et al., 2008; Heras and Larrosa, 2006; Li et al., 2007; Kuegel, 2010] by the clause branching suggested by the extension rule: instead of branching on a variable x and its negation x, select a clause l1_· · ·_ lr in the current formula and create r branches, one branch for each literal from ¶l1↪ ▷ ▷ ▷ ↪ lr♦, and proceed as usual in BnB MaxSAT solvers.

On the other hand, the algorithm of Figure 3 can be drastically improved by incorporating solving techniques that implement BnB MaxSAT solvers such as the computation of an initial upper bound with local search [Cai et al., 2014], the computation at each node of a lower bound by detecting disjoint subsets of inconsistent formulas with a linear-time procedure that applies unit resolution [Li et al., 2010; 2005; 2006], and heuristics for selecting the clause to be expanded.

Note that the suggested clause branching for MaxSAT is not valid for MinSAT [Ignatiev et al., 2016; Li et al., 2011; 2012], because the extension rule preserves the minimum number of falsified clauses among the newly created branches but does not preserve the maximum number of falsified clauses. This also implies that the proposed calculus is unsound for MinSAT. Recall that MinSAT for a multiset of clauses φ is to find an assignment that maximizes the number of falsified clauses in φ.

Finally, it is worth mentioning that the described tableaubased algorithm only needs polynomial space, while existing variable elimination algorithms based on MaxSAT resolution require exponential memory space [Bonet et al., 2007].

5 Extension toWMaxSAT andWPMaxSAT

Many practical optimization problems admit more compact and natural MaxSAT 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 presented the tableau method for unweighted MaxSAT, but the proposed tableau calculus can be extended to solve both WMaxSAT and WPMaxSAT.

In the case of WMaxSAT, we should keep in mind that a weighted clause (c↪w) is equivalent to have w copies of the unweighted clause c. So, the application of the contradiction rule to two unit clauses (l↪w1)↪ (l↪w2) amounts to adding an unmarked empty clause with weight w = min(w1↪ w2) (i.e.; (⇤↪ w)), declare the clauses (l↪ w1)↪ (l↪ w2) to be marked, and add the unmarked clauses (l↪ w1 - w) and (l↪ w2 - w) in the newly created branch. The application of the extension rule to a weighted clause (l1 _ · · · _ lr↪w), amounts to append r nodes below the current branch, labelling each node with a different unit weighted clause from ¶(l1↪ w)↪ ▷ ▷ ▷ ↪ (lr↪ w)♦. Finally, to get a complete calculus, we need to define a contraction rule: if a branch contains two unmarked clauses (C↪w1) and (C↪ w2), mark these clauses and add the unmarked clause (C↪ w1 + w2) in the newly created branch.

Example 4 Let φ be the multiset of weighted clauses ¶(x1↪ 3)↪ (x2↪ 2)↪ (x1 _ x2↪ 2)♦. Figure 4 shows a saturated clause tableau T for φ. We first apply the extension rule to (x1 _ x2↪ 2) and derive two new branches. In the leftmost branch, the application of the contradiction rule to (x1↪ 3) and (x1↪ 2) yields (⇤↪ 2) and (x1↪ 1). In the rightmost branch, the application of the contradiction rule to (x2↪ 2) and (x2↪ 2) yields (⇤↪ 2). The two saturated branches of the tableau have cost 2. The unmarked clauses in each branch are: ¶(x2↪ 2)↪ (⇤↪ 2)↪ (x1↪ 1)♦ (branch 1), and ¶(x1↪ 3)↪ (⇤↪ 2)♦ (branch 2). Therefore, the minimum sum of weights of falsified clauses in φ is 2.

In the case of WPMaxSAT, we should add, to each hard clause, a weight greater than the sum of weights of the input soft clauses, and proceed as in WMaxSAT but ignoring those branches in which a contradiction is detected in hard clauses.

6 Conclusions

We defined a sound and complete clause tableau calculus for WPMaxSAT that is simpler and more intuitive than MaxSAT resolution because it avoids the use of compensation clauses. At the same time, the contributions of the paper provide a new angle to look at MaxSAT, as well as to compare the inference in SAT with the inference in MaxSAT. Interestingly, an immediate application of our results could be the incorporation of the defined clause branching into BnB MaxSAT solvers.

As future work we plan to define a complete tableau calculus for MinSAT, and extend our results to both non-CNF formulas and first-order clauses.