Josep Argelich

Felip Manyà

Joan Ramon Soler

Clause tableaux for maximum and minimum satisfiability

Keywords: Boolean optimization, MaxSAT, MinSAT, tableaux, calculus, completeness

The inference systems proposed for solving SAT are unsound for solving MaxSAT and MinSAT, because they preserve satisfiability but not the minimum and maximum number of clauses that can be falsified, respectively. To address this problem, we first define a clause tableau calculus for MaxSAT and prove its soundness and completeness. We then define a clause tableau calculus for MinSAT and also prove its soundness and completeness. Finally, we define a complete clause tableau calculus for solving both MaxSAT and MinSAT, in that the minimum number of generated empty clauses provides an optimal MaxSAT solution and the maximum number provides an optimal MinSAT solution.

Introduction

MaxSAT and MinSAT are nowadays competitive generic problem solving approaches that are able to solve challenging optimization problems in different areas (see e.g. [2-7, 15, 17, 19, 21, 23, 27-34] and the references therein for related work). MaxSAT is to find a truth assignment that minimizes the number of unsatisfied clauses in a multiset of clauses, while MinSAT is to find a truth assignment that maximizes the number of unsatisfied clauses.

The inference systems proposed for solving SAT are unsound for solving MaxSAT and MinSAT, because they preserve satisfiability but not the maximum and minimum number of clauses that can be falsified. Thus, we first need to define inference rules meeting that condition and then show that their correct application allows one to derive as many empty clauses as the minimum number of clauses that can be falsified in the case of MaxSAT, and as the maximum number of clauses that can be falsified in the case of MinSAT.

Resolution-style calculus have been defined for MaxSAT [START_REF] Bonet | A complete calculus for Max-SAT[END_REF][START_REF] Bonet | Resolution for max-SAT[END_REF][START_REF] Larrosa | Resolution in Max-SAT and its relation to local consistency in weighted CSPs[END_REF] and MinSAT [START_REF] Li | An exact inference scheme for MinSAT[END_REF], and the proposed variable elimination algorithms provide optimal solutions. The MaxSAT and MinSAT resolution rule states that the complementary clauses x ∨ l 1 1

∨ • • • ∨ l 1 m and ¬x ∨ l 2 1 ∨ • • • ∨ l 2
n can be replaced with the usual resolvent

l 1 1 ∨ • • • ∨ l 1 m ∨ l 2 1 ∨ • • • ∨ l 2
n and the following m + n compensation clauses:

x ∨ l 1 1 ∨ • • • ∨ l 1 m ∨ ¬l 2 1 , . . ., x ∨ l 1 1 ∨ • • • ∨ l 1 m ∨ l 2 1 ∨ • • • ∨ l 2 n-1 ∨ ¬l 2 n , ¬x ∨ l 2 1 ∨ • • • ∨ l 2 n ∨ ¬l 1 1 , . . ., ¬x ∨ l 2 1 ∨ • • • ∨ l 2 n ∨ l 1 1 ∨ • • • ∨ l 1 m-1 ∨ ¬l 1 m .
The role of the compensation clauses is to ensure that the two parent clauses are replaced by a collection of clauses that preserve the number of unsatisfied clauses. The difference between MaxSAT and MinSAT lies in the way the variable elimination algorithms saturate the variables. Refinements of the previous resolution rule have been incorporated into branch-and-bound MaxSAT and MinSAT algorithms and have produced important speedups [START_REF] Abramé | Local Max-Resolution in branch and bound solvers for Max-SAT[END_REF][START_REF] Abramé | On the resiliency of unit propagation to Max-Resolution[END_REF][START_REF] Larrosa | Resolution in Max-SAT and its relation to local consistency in weighted CSPs[END_REF][START_REF] Li | Resolution-based lower bounds in MaxSAT[END_REF][START_REF] Li | New inference rules for max-SAT[END_REF][START_REF] Li | Optimizing with minimum satisfiability[END_REF].

In this paper, we first extend the clause tableau calculus for SAT [START_REF] Agostino | Tableaux methods for classical propositional logic[END_REF][START_REF] Hähnle | Tableaux and related methods[END_REF] to solve both MaxSAT [START_REF] Li | A clause tableaux calculus for MaxSAT[END_REF] and MinSAT [START_REF] Li | A clause tableau calculus for MinSAT[END_REF]. An essential issue to address is how to derive simpler subproblems in such a way that the minimum/maximum number of unsatisfied clauses is preserved. The proposed clause MaxSAT tableau calculus and the clause SAT tableau calculus are quite similar, in that they use the same rules but applied differently. The clause MinSAT tableau calculus has an inference rule that does not resemble the rules of the SAT and MaxSAT calculi. It is worth noticing that a clause MinSAT tableau calculus must be able to derive contradictions from satisfiable instances because they can have interpretations that falsify some clauses.

From the insights gained after analysing clause MaxSAT and MinSAT tableaux, we then propose a clause tableau calculus that is valid for both MaxSAT and MinSAT. It preserves adequately the number of unsatisfied clauses in the generated subproblems. The leaf nodes of a completed search tree contain a number of empty clauses ranging between the minimum and the maximum number of unsatisfied clauses in the input formula, and there is at least one branch with the minimum value and there is at least one branch with the maximum value. This calculus also provides optimal MaxSAT and MinSAT assignments by inspecting the optimal branches. This is a journal version of three conference papers. It unifies results on clause MaxSAT tableaux appeared in [START_REF] Li | A clause tableaux calculus for MaxSAT[END_REF], on clause MinSAT tableaux appeared in [START_REF] Li | A clause tableau calculus for MinSAT[END_REF] and on a tableau-based procedure for MaxSAT and MinSAT appeared in [START_REF] Argelich | Clause branching in MaxSAT and MinSAT[END_REF].

The paper is structured as follows. Section 2 defines basic concepts. Section 3 reviews how clause tableaux can be used to solve SAT. Section 4 defines a complete clause tableau calculus for MaxSAT. Section 5 defines a complete clause tableau calculus for MinSAT. Section 6 describes a complete clause tableau calculus that is valid for both MaxSAT and MinSAT. Section 7 gives the conclusions.

Preliminaries

Given a set of propositional variables {x 1 , . . . , x n }, a literal is a variable x i or its negation ¬x i . A weighted clause is a pair (c, w), where c is a disjunction of literals and w, its weight, is a positive integer.

A truth assignment assigns to each variable either 0 (false) or 1 (true). It satisfies literal x i (¬x i ) if x i evaluates to 1 (0), it satisfies weighted clause (c, w) if it satisfies a literal of c and it satisfies a multiset of clauses if it satisfies all its clauses. The weight w is the penalty of violating clause c. When all clauses have the same weight, their weights are omitted.

The Weighted Partial MaxSAT problem, or WPMaxSAT, for a multiset of clauses φ is to find an assignment that satisfies all the hard clauses and minimizes the sum of the weights of the unsatisfied soft clauses. The most common subproblems of WPMaxSAT are the following ones: Weighted MaxSAT (WMaxSAT), which is WPMaxSAT without hard clauses; Partial MaxSAT (PMaxSAT), which is WPMaxSAT when all the soft clauses have the same weight; and MaxSAT, which is PMaxSAT without hard clauses.

The Weighted Partial MinSAT problem, or WPMinSAT, for a multiset of clauses φ is to find an assignment that satisfies all the hard clauses and maximizes the sum of the weights of the unsatisfied soft clauses. The most common subproblems of WPMinSAT are the following ones: Weighted MinSAT (WMinSAT), which is WPMinSAT without hard clauses; Partial MinSAT (PMinSAT), We represent MaxSAT and MinSAT instances as multisets of clauses. Repeated clauses cannot be collapsed into one clause as in SAT, because then the maximum/minimum number of unsatisfied clauses might not be preserved. For example, the multiset of unit clauses {x 1 , ¬x 1 , x 1 , ¬x 1 } has a minimum of two unsatisfied clauses while {x 1 , ¬x 1 } has just one unsatisfied clause. In fact, {x 1 , ¬x 1 , x 1 , ¬x 1 } is equivalent to the multiset of weighted clauses {(x 1 , 2), (¬x 1 , 2)}. Clauses can be represented by the set of its literals as in SAT because repeated literals can be collapsed into one literal without affecting the preservation of the number of unsatisfied clauses.

Let φ be a multiset of clauses and let l 1 , . . . , l r be literals that occur in φ. The instantiation of l 1 , . . . , l r in φ, denoted by φ l 1 |•••|l r , is the multiset of clauses resulting of eliminating from φ all the occurrences of ¬l 1 , . . . , ¬l r and removing all the clauses with occurrences of l 1 , . . . , l r .

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 [START_REF] Fitting | First-Order Logic and Automated Theorem Proving[END_REF][START_REF] Smullyan | First-Order Logic[END_REF]. 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 1 , . . . , C m }, we start by creating an initial tableau that has a single branch with m nodes, where each node is labelled with a clause of φ. This process is known as the application of the initial tableau rule. Then, we select an open branch B and a clause l 1 ∨ . . . ∨ l r of φ with r ≥ 2 that has not yet been expanded in B and append r sibling nodes below B, labelling each node with a different unit clause from {l 1 , . . . , l r }. 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 by applying the contradiction rule. In this paper, closing a branch amounts to deriving an empty clause. 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. The set of clauses φ is declared to be unsatisfiable in the first case and satisfiable in the second case. Table 1 shows the expansion rules of a complete clause tableau calculus for SAT. EXAMPLE 3.1 To determine the satisfiability of φ = {x 1 , ¬x 1 ∨ x 2 , ¬x 1 ∨ ¬x 2 } with clause tableaux we start by creating the initial tableau (T 0 ), We then expand the second node (T 1 ) and close the leftmost branch by applying the contradiction rule to x 1 and ¬x 1 , obtaining another clause tableau (T 2 ): Finally, we expand the third node on the rightmost branch (T 3 ) and close the new leftmost (T 4 ) and rightmost branches (T 5 ), obtaining a clause tableau proof of the unsatisfiability of φ, Formally, a clause tableau proof of the unsatisfiability of a set of clauses φ is a sequence of clause tableaux T 0 , . . . , T n such that T 0 is an initial tableau of φ, T n is a closed tableau and T i has been obtained by a single application of the extension or contradiction rule on an open branch of T i-1 for i = 1, . . . , n. In a proof of satisfiability, T n 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 T n is a clause tableau proof because it collapses all the sequence of tableaux. In Example 3.1, the sequence T 0 , T 1 , T 2 , T 3 , T 4 , T 5 is a clause tableau proof, although T 5 alone is also considered to be a proof.

We say that a clause tableau is completed when all its branches are closed or it contains an open branch in which it was not possible to detect a contradiction with the expansion rules of Table 1.

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

Clause tableaux for MaxSAT

The clause SAT tableau calculus is not valid for solving MaxSAT, but it can become sound and complete by applying differently the expansion rules of Table 1.

Firstly, the application of expansion rules in a branch cannot stop once a contradiction is detected. Since the aim of MaxSAT is to derive all the possible contradictions, the application of rules in a branch should continue until no more expansion rules can be applied. Thus, a different notion of completed tableau is needed.

Secondly, the application of rules in SAT leads to accumulate the newly added unit clauses in the branch in such a way that satisfiability is preserved in at least one branch when the input set of clauses is satisfiable. However, the addition of redundant clauses can lead to wrong MaxSAT solutions. In clause MaxSAT tableaux, the goal should be to keep the minimum number of unsatisfied clauses in at least one branch and not to decrease that number in the rest of branches. As we show below, the rules of Table 1 satisfy that condition provided that we maintain active and inactive clauses. In other words, once a clause has been used as a premise of a rule in a branch, it cannot be used again in that branch and becomes inactive. For example, thanks to distinguishing between active and inactive clauses, we will detect one contradiction in the multiset of unit clauses {x 1 , ¬x 1 , ¬x 1 } and two in {x 1 , x 1 , ¬x 1 , ¬x 1 }. Without that, we could detect two contradictions in the first case, obtaining a wrong answer. In fact, the inference rules of MaxSAT can be seen as rewriting rules. DEFINITION 4.1 A clause MaxSAT tableau is a tree with a finite number of branches whose nodes are labelled with clauses. A branch is a maximal path in a tree, and we assume that branches have a finite number of nodes. Let T be a clause MaxSAT tableau for a multiset of clauses φ, and let B be a branch of T. Branch B is saturated when all its active clauses are unit or empty, and the contradiction rule cannot be further applied on B. Tableau T is completed iff all its branches are saturated. The cost of a saturated branch is the number of empty clauses in it. The cost of a completed clause MaxSAT tableau is the minimum cost among all its branches.

The notion of saturation is crucial in MaxSAT because it indicates that the application of expansion 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 any completed clause MaxSAT tableau for φ is k. So, the systematic construction of a completed clause MaxSAT tableau for φ provides an exact method for MaxSAT, and each completed tableau is a proof. EXAMPLE 4.4 Let φ = {¬x 1 , ¬x 2 , ¬x 3 , x 1 ∨x 2 , x 1 ∨x 3 , x 2 ∨x 3 } be a multiset of clauses. Figure 1 shows a completed clause MaxSAT 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 x 1 ∨x 2 and declare it inactive in the newly created branches (in the figure we write in bold the inactive clauses in the leftmost branch, which is the branch on which we concentrate in this example). Thirdly, we apply the contradiction rule to ¬x 1 and x 1 and declare these clauses inactive in the leftmost branch. Fourthly, we apply the extension rule to x 1 ∨ x 3 and declare it inactive in the newly created branches. Fifthly, we apply the extension rule to x 2 ∨ x 3 and declare it inactive. Sixthly, we apply the contradiction rule to ¬x 2 and x 2 and declare these clauses inactive in the leftmost branch. No more inference rules can be applied on the leftmost branch, and therefore, the branch is saturated, having as active clauses { , , x 1 , ¬x 3 }. 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 active clauses in each branch are { , , x 1 , ¬x 3 } (branch 1), { , , x 1 , ¬x 2 } (branch 2), { , , } (branch 3), { , , ¬x 2 , x 3 } (branch 4), { , , x 2 , ¬x 3 } (branch 5), { , , } (branch 6), { , , ¬x 1 , x 2 } (branch 7) and { , , ¬x 1 , x 3 } (branch 8). Therefore, the minimum number of unsatisfied clauses in φ is 2.

Soundness and completeness of clause MaxSAT tableaux

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

FIGURE 1. A completed clause MaxSAT tableau for φ = {¬x 1 , ¬x 2 , ¬x 3 , x 1 ∨ x 2 , x 1 ∨ x 3 , x 2 ∨ x 3 }
that proves that the minimum number of unsatisfied clauses in φ is 2. THEOREM 4.5 Soundness. Let φ be a multiset of clauses, and let T be a completed clause MaxSAT tableau for φ of cost m. Then, the minimum number of clauses that can be falsified in φ is m.

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

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

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

Since T i was constructed from T i-1 by applying either the contradiction rule or the extension rule on a branch B of T i-1 and the rest of branches of T i-1 remain unchanged in T i , we just need to prove that I satisfies the same number of active clauses in B and in at least one of the newly created

φ = {¬x 1 , ¬x 2 , ¬x 3 , x 1 ∨ x 2 , x 1 ∨ x 3 , x 2 ∨ x 3 } from Example 4.7.
branches and does not decrease that number in the rest of newly created branches. We distinguish two cases:

• We proved that the minimum number of active clauses that I falsifies among the branches of T 0 , . . . , T n -and in particular of T-is k, but this is in contradiction with T being a completed MaxSAT tableau for φ that has cost m; since T is completed, the active 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 active 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. PROOF. Each clause MaxSAT tableau for φ can be completed after a finite number of steps. This follows from the fact that the number of applications of extension rules in a branch is bound by the number of clauses in the input multiset and the number of applications of the contradiction rules is bounded by the number of literals occurring in the input multiset.

Assume that there is a completed MaxSAT 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 active 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: (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 unsatisfied clauses, T must have a saturated branch of cost m.

I(x) = 1 (I(x) = 0) if x (¬x)
Hence, each completed clause MaxSAT tableau T for a multiset of clauses φ has cost m if the minimum number of clauses that can be falsified in φ is m.

From the proof of Theorem 4.6, it follows that we can derive an optimal MaxSAT assignment I from a saturated branch B of minimum cost. The optimal assignment I sets a variable x to 1 (0) if B has a node labelled with the active clause x (¬x); the rest of variables can be set to either 0 or 1.

Clause tableaux for WMaxSAT and WPMaxSAT

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 clause tableaux for unweighted MaxSAT, but the proposed 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 having w copies of the unweighted clause c. So, the application of the contradiction rule to two unit clauses (l, w 1 ), (¬l, w 2 ) amounts to adding an active empty clause with weight w = min(w 1 , w 2 ) (i.e.; ( , w)), declare the clauses (l, w 1 ), (¬l, w 2 ) to be inactive and add the active clauses (l, w 1w) and (¬l, w 2w) in the newly created branch. Clauses with weight 0 are not added. The application of the extension rule to a weighted clause (l 1 ∨ • • • ∨ l r , w) amounts to appending r nodes below the current branch, labelling each node with a different unit weighted clause from {(l 1 , w), . . . , (l r , w)}. Finally, to get a complete calculus, we need to define a contraction rule: if a branch contains two active clauses (C, w 1 ) and (C, w 2 ), inactivate these clauses and add the active clause (C, w 1 + w 2 ) in the newly created branch. EXAMPLE 4.7 Let φ = {(¬x 1 , 3), (¬x 2 , 2), (x 1 ∨ x 2 , 2)} be a multiset of weighted clauses. Figure 3 shows a completed clause WMaxSAT tableau T for φ. We first apply the extension rule to (x 1 ∨ x 2 , 2) and FIGURE 3. A completed clause WMaxSAT tableau for the multiset of weighted clauses φ = {(¬x 1 , 3), (¬x 2 , 2), (x 1 ∨ x 2 , 2)} that proves that the minimum sum of weights of unsatisfied clauses in φ is 2.

derive two new branches. In the leftmost branch, the application of the contradiction rule to (¬x 1 , 3) and (x 1 , 2) yields ( , 2) and (¬x 1 , 1). In the rightmost branch, the application of the contradiction rule to (¬x 2 , 2) and (x 2 , 2) yields ( , 2). The two saturated branches of the tableau have cost 2. The active clauses in each branch are {(¬x 2 , 2), ( , 2), (¬x 1 , 1)} (left branch) and {(¬x 1 , 3), ( , 2)} (right branch). Therefore, the minimum sum of weights of unsatisfied 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. Moreover, we could prune those branches in which a contradiction is detected between hard clauses or clauses derived from hard clauses.

Clause tableaux for MinSAT

We showed in the previous section that the minimum number of empty clauses among the branches of a completed clause MaxSAT tableau for a multiset of clauses φ is equal to the number of clauses falsified by an optimal MaxSAT assignment of φ. Nevertheless, the maximum number of empty clauses among the branches of a completed clause MaxSAT tableau for φ is not the maximum number of clauses that can be falsified in φ, i.e. clause MaxSAT tableaux cannot solve MinSAT. This is so because the extension rule is unsound for MinSAT in the sense that it does not preserve the maximum number of clauses that can be falsified.

In the rest of the section, we first define a clause MinSAT tableau calculus that incorporates a sound extension rule. We then prove the soundness and completeness of the proposed calculus. Finally, we present how our results can be extended to deal with WMinSAT and WPMinSAT instances. Note that, in MinSAT, we also need to derive contradictions from satisfiable instances because the maximum number of clauses that can be falsified in a satisfiable instance other than the empty multiset is always greater than or equal to one. DEFINITION 5.1 A clause MinSAT tableau is a finite tree whose nodes are labelled with multisets of clauses. A branch is a maximal path in a tree. In the definition of the extension rule, note that

φ ¬l 1 |•••|¬l r = { } ∪ φ ¬l 1 |•••|¬l r . DEFINITION 5.3
Let T be a clause MinSAT tableau for a multiset of clauses φ, and let B be a branch of T. Branch B is saturated iff its leaf node is labelled with the empty multiset or with a multiset of empty clauses. Tableau T is completed iff all its branches are saturated. The cost of a saturated branch is the number of empty clauses in its leaf node. The cost of a completed clause MinSAT tableau is the maximum cost among all its branches.

EXAMPLE 5.4

Let

φ 1 = {¬x 1 , ¬x 2 , x 1 ∨ x 2 } and φ 2 = {x 1 ∨ x 2 , ¬x 1 ∨ x 3 , ¬x 2 ∨ ¬x 3 } be multisets of clauses.
Figures 4 and5 show completed clause MinSAT tableaux for φ 1 and φ 2 , respectively. The leaf nodes of the branches of the tableau for φ 1 have at most cost 2 and of the tableau for φ 2 have at most cost 1. Therefore, the maximum number of clauses that can be falsified in φ 1 is 2 and in φ 2 is 1. Note that φ 2 is satisfiable.

Soundness and completeness of clause MinSAT tableaux

We first prove that the extension rule preserves the maximum number of unsatisfied clauses among the branches of a clause MinSAT tableau and then the soundness and completeness of the clause MinSAT tableau calculus. PROOF. We first prove the following inequalities: minsat(φ) ≥ minsat(φ ) and minsat(φ

) ≥ minsat(φ ¬l 1 |•••|¬l r ).
Since φ ⊂ φ and the maximum number of clauses that can be falsified in every subset of φ cannot be greater than the maximum number of clauses that can be falsified in φ, it holds that minsat(φ) ≥ minsat(φ ).

Assume that there is an optimal assignment I of φ ¬l 1 |•••|¬l r that falsifies more clauses than an optimal assignment I of φ. Then, we could extend I by setting I (l i ) = 0 for i = 1, . . . , r and get an optimal assignment of φ that falsifies more clauses than I; if we restore the occurrences of the literals l 1 , . . . , l r in the clauses of φ ¬l 1 |•••|¬l r in which such literals were eliminated when ¬l 1 , . . . , ¬l r were instantiated in φ, we get a multiset φ such that φ ⊆ φ. It holds that the number of clauses that I falsifies in φ ¬l 1 |•••|¬l r and φ is the same because I falsifies the added literals, but this is in contradiction with I being optimal. Therefore, minsat(φ) ≥ minsat(φ

¬l 1 |•••|¬l r ).
Taking into account the previous inequalities, we prove that minsat(φ) = max(minsat(φ ), minsat(φ ¬l 1 |•••|¬l r )). Let I be an optimal assignment of φ. We distinguish two cases: i) I satisfies l 1 ∨ • • • ∨ l r . Then, I falsifies the same clauses in φ and φ and is also an optimal assignment of φ because minsat(φ) ≥ minsat(φ ). Since minsat(φ) = minsat(φ ) and minsat(φ

) ≥ minsat(φ ¬l 1 |•••|¬l r ), it follows that minsat(φ) = max(minsat(φ ), minsat(φ ¬l 1 |•••|¬l r )). ii) I falsifies l 1 ∨ • • • ∨ l r .
Then, I sets l 1 , . . . , l r to 0, and I falsifies the same number of clauses in φ and

φ ¬l 1 |•••|¬l r . Since minsat(φ) ≥ minsat(φ ¬l 1 |•••|¬l r ), it follows that I is also an optimal assignment of φ ¬l 1 |•••|¬l r . Since minsat(φ) = minsat(φ ¬l 1 |•••|¬l r ) and minsat(φ) ≥ minsat(φ ), it follows that minsat(φ) = max(minsat(φ ), minsat(φ ¬l 1 |•••|¬l r )).
THEOREM 5.6 Soundness. Let φ be a multiset of clauses, and let T be a completed clause MinSAT tableau for φ that has cost m. Then, the maximum number of clauses that can be falsified in φ is m.

PROOF. The clause MinSAT tableau T was obtained by creating a sequence of clause MinSAT tableaux T 0 , . . . , T n (n ≥ 0) such that T 0 is an initial tableau for φ, T n = T, and T i was obtained by a single application of the extension rule on a leaf node of a branch of T i-1 for i = 1, . . . , n. Assume that I is an optimal assignment of φ that falsifies k clauses, where k = m. By induction on n, we Downloaded from https://academic.oup.com/jigpal/advance-article-abstract/doi/10.1093/jigpal/jzz025/5544641 by guest on 18 February 2020 prove that the maximum number of clauses that I falsifies among the leaf nodes of the branches of T 0 , . . . , T n (and in particular of T) is k:

Basis: T 0 has a single branch with one node labelled with the clauses of φ. So, I falsifies k clauses in T 0 , and k is the maximum number of clauses that can be falsified in T 0 .

Inductive step: assume that the maximum number of clauses that I falsifies among the leaf nodes of the branches of T i-1 is k. We prove that the maximum number of clauses that I falsifies among the leaf nodes of the branches of T i is also k.

T i was constructed from T i-1 by applying the extension rule on a branch B of T i-1 . If I falsifies k clauses of the leaf node of B, by Lemma 1, the maximum number of clauses that I falsifies among the branches of T i remains k. If I falsifies r clauses of the leaf node of B, where r < k, then I falsifies k clauses of the leaf node of a branch B of T i (B = B and B is also a branch of T i-1 ), and I cannot falsify more than k clauses in the leaf nodes of any of the two branches derived from B because otherwise we could define an assignment that falsifies more than k clauses of the leaf node of B.

We proved that the maximum number of clauses that I falsifies among the leaf nodes of the branches of T 0 , . . . , T n -and in particular of T-is k, but this is in contradiction with T being a completed clause MinSAT tableau for φ that has cost m. Since T is completed and has cost m, the leaf nodes are labelled with either a multiset of empty clauses or the empty formula, and there is at least a branch B whose leaf node is a multiset with m empty clauses. So, the maximum number of clauses that can be falsified in the leaf node of B is m (and not k) and is, at most, m in the rest of leaf nodes of branches of T. Hence, the maximum number of clauses that can be falsified in φ is m. THEOREM 5.7 Completeness. Let φ be a multiset of clauses whose maximum number of clauses that can be falsified in φ is m. Then, any completed clause MinSAT tableau for φ has cost m. PROOF. Each clause MinSAT tableau T for φ can be completed after a finite number of steps. This follows from the fact that the extension rule either eliminates one clause or replaces one clause with an empty clause at each application of the rule. Moreover, the instantiation of literals neither increases the number of clauses nor increases the number of literals per clause. Thus, after a finite number of applications of the extension rule, T is transformed into a completed clause MinSAT tableau.

Assume that there is a completed clause MinSAT 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 leaf node of B has k empty clauses, and each empty clause is derived from a clause of φ; let C 1 , . . . , C k be such clauses. We define an assignment I of φ as follows:

I(x) = 1 (I(x) = 0) if ¬x (x) occurs in {C 1 , . . . , C k }, and I(x) = 0 if variable x does not occur in {C 1 , . . . , C k }. Note that {C 1 , . . . , C k }
only contain literals with both the same variable and polarity because the corresponding literals with opposite polarity occur in clauses that were eliminated. Assignment I falsifies at least k clauses of φ because each literal occurring in {C 1 , . . . , C k } is unsatisfied by I. Since k > m, this is in contradiction with m being the maximum number of clauses that can be falsified in φ.

(ii) T has no branch of cost m. This is in contradiction with m being the maximum number of clauses that can be falsified in φ. Since an optimal assignment falsifies m clauses of the initial tableau and the leaf nodes of a completed clause MinSAT tableau are labelled with either a multiset of empty clauses or the empty formula, by Lemma 5.5, T must have a branch of cost m.

From the proof of Theorem 5.7 it follows that, for building an optimal assignment I from a completed tableau, we have to consider a branch with a maximum number of empty clauses in its leaf node and identify the input clauses that became empty. Then, for each one of such clauses, say l 1 ∨ • • • ∨ l m , we define I(l i ) = 0 for i = 1, . . . , m, and the variables that do not appear in such clauses can be set to an arbitrary value. For example, in the tableau for φ 1 = {¬x 1 , ¬x 2 , x 1 ∨ x 2 } of Figure 4, the input clauses that became empty in the branch with maximum cost are {¬x 1 , ¬x 2 }, and therefore, I(x 1 ) = I(x 2 ) = 1 is an optimal assignment of φ 1 .

Clause tableaux for WMinSAT and WPMinSAT

We presented clause tableaux for unweighted MinSAT to keep the description as simple as possible. We now describe how the clause MinSAT tableau calculus can be extended to deal with WMinSAT and WPMinSAT instances.

In the case of WMinSAT, we use the same tableau rules but keeping the weights of the clauses. Note that the extension rule either removes clauses or eliminates literals. When a literal is eliminated from a clause, the shortened clause maintains the same weight. In addition, we also could need to collapse several weighted clauses of the form (C, w 1 ), . . . , (C, w k ) into a single weighted clause

(C, w 1 + • • • + w k ).
EXAMPLE 5.8 Let φ = {(x 1 , 1), (¬x 2 , 3), (x 1 ∨ ¬x 2 , 5), (x 1 ∨ ¬x 3 , 2), (x 2 ∨ x 3 , 1)} be a multiset of weighted clauses. Figure 6 shows a completed clause WMinSAT tableau T for φ. The leaf nodes of the branches of T have at most cost 11. Therefore, the maximum sum of the weights of the clauses that can be falsified in φ is 11.

In the case of WPMinSAT, we must first derive an equivalent WMinSAT instance and then solve the derived instance as explained above. We will assume that there is an assignment that satisfies all the hard clauses, since otherwise no feasible 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 (¬l 1 , w + 1), (l 1 ∨ ¬l 2 , w + 1), . . ., (l

1 ∨ l 2 ∨ • • • ∨ ¬l k , w + 1) for each hard clause h = l 1 ∨ l 2 ∨ • • • ∨ l k in φ.
Observe that an assignment I satisfies h iff I falsifies exactly one clause among ¬l 1 , l 1 ∨ ¬l 2 , . . . , l 1 ∨ l 2 ∨ • • • ∨ ¬l k , or equivalently, I falsifies h iff I satisfies all these clauses. Since the clauses derived from hard clauses have weight w + 1 and we assumed that 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 unsatisfied clauses in φ is m, then the maximum sum of the weights of the unsatisfied clauses in φ is m-#hard×(w+1). The treatment of hard clauses in MinSAT tableaux is not as in MaxSAT tableaux, where it is enough to add the weight w + 1 to each hard clause and solve the resulting WMaxSAT instance.

Clause tableaux for MaxSAT and MinSAT

After defining a clause tableau calculus for MaxSAT and another for MinSAT, a natural question to ask is whether there exists a calculus that is valid for both MaxSAT and MinSAT. In this section, we propose a tableau calculus for MaxSAT and MinSAT that preserves adequately the number of unsatisfied clauses in the generated subproblems. The leaf nodes of a completed tableau contain a number of empty clauses ranging between the minimum and the maximum number of unsatisfied clauses in the input formula, and there is at least one branch with the minimum value and at least one branch with the maximum value. This scheme also generates optimal MaxSAT and MinSAT assignments by inspecting the optimal branches.

A natural extension of clause tableaux is to perform some kind of local inference at each node, as in fact MinSAT tableaux do in one of the branches when assigning the variables occurring in a select clause to force its violation. In SAT, assuming that the initial tableau contains a single node with the input set of clauses, we can introduce local inference by applying the following extension rule: if the leaf node of a branch B is labelled with the set of clauses φ = φ ∪ {l 1 ∨ • • • ∨ l k }, then append k sibling nodes below B labelled with φ l 1 , . . . , φ l k . Then, the input set of clauses is unsatisfiable iff the empty clause has been derived in each branch. Actually, if the local inference applied is unit propagation instead of the instantiation of literal l i (i.e., φ l i ), also known as unit clause rule, we get the DPLL procedure [START_REF] Davis | A machine program for theorem-proving[END_REF] with clause branching [START_REF] Hooker | Branching rules for satisfiability[END_REF].

Unfortunately, the outlined SAT approach is unsound for MaxSAT and MinSAT because it does not preserve neither the maximum nor the minimum number of unsatisfied clause. For example, if we consider the multiset of clauses φ = {¬x 1 , ¬x 1 , ¬x 2 , ¬x 2 , x 1 ∨ x 2 }, the generated tableau has two leaf nodes with two empty clauses, as Figure 7 shows. Note that we first branch on x 1 (labelling the node with φ x 1 ) and x 2 (labelling the node with φ x 2 ) and then instantiate ¬x 2 in the left branch and ¬x 1 in the right branch. However, the MaxSAT solution of φ is one and the MinSAT solution is four. Also note that branching on l 1 , . . . , l k is sound in MaxSAT tableaux but becomes unsound when local inference is added to each node.

The key point to integrate MaxSAT and MinSAT is to define an extension rule that preserves both the maximum and the minimum number of unsatisfied clause. This is what we do in the clause MaxMinSAT tableau defined below. DEFINITION 6.1 A clause MaxMinSAT tableau is a finite tree whose nodes are labelled with multisets of clauses. A branch is a maximal path in a tree. DEFINITION 6.2 Let φ be a multiset of clauses. A clause MaxMinSAT tableau for φ is constructed by a sequence of applications of the following rules:

Initialize A tree with a single branch with a single node labelled with the multiset of clauses φ is a clause MaxMinSAT tableau for φ. Such a tableau is called initial tableau. Extension Given a clause tableau T for φ, and a branch B of T whose leaf node is labelled with a multiset φ = φ ∪ {l Tableau T is completed iff all its branches are saturated. The cost of a saturated branch is the number of empty clauses in its leaf node. The MaxSAT cost of a completed clause MaxMinSAT tableau is the minimum cost among all its branches, and the MinSAT cost of a completed clause MaxMinSAT tableau is the maximum cost among all its branches.

We prove below that the branches with MaxSAT and MinSAT costs provide optimal MaxSAT and MinSAT solutions, respectively. EXAMPLE 6. [START_REF] Ansótegui | Exploiting subproblem optimization in SAT-based MaxSAT algorithms[END_REF] We consider again the multiset of clauses φ = {¬x 1 , ¬x 1 , ¬x 2 , ¬x 2 , x 1 ∨ x 2 } of Figure 7. Figure 8 displays a completed clause MaxMinSAT tableau for φ. The MaxSAT cost of the tableau is 1 and the MinSAT cost is 4. Hence, the minimum number of clauses that can be falsified in φ is 1, and the maximum number is 4.

The next two lemmas prove that the MaxMinSAT extension rule preserves both the maximum and the minimum number of unsatisfied clauses. In other words, we prove its soundness. Based on these results, we then prove the completeness of the clause MaxMinSAT tableau calculus. LEMMA 6.5 MaxSAT clause branching. Let φ be a multiset of clauses, let l 1 ∨ • • • ∨ l k be a clause of φ and let maxsat(φ) be the minimum number of unsatisfied clauses in φ. Then, maxsat(φ) = min(maxsat(φ l 1 ), . . . , maxsat(φ l k ), maxsat(φ ¬l 1 ,...,¬l k )).

( 1 )

PROOF. Let I be an optimal MaxSAT assignment. We prove that the minimum number of unsatisfied clauses in φ is the same as the minimum number of unsatisfied clauses in at least one of the multisets φ l 1 , . . . , φ l k , φ ¬l 1 ,...,¬l k and is not smaller in the rest of multisets. We distinguish two cases: 1. I satisfies l 1 ∨ • • • ∨ l k : if I satisfies l i , 1 ≤ i ≤ k, then maxsat(φ) = maxsat(φ l i ) because deleting the clauses containing l i and removing the occurrences of ¬l i preserve the number of unsatisfied clauses between φ and φ l i for every assignment. Since at least one literal l i is satisfied by I, the minimum number of unsatisfied clauses is preserved in one of the derived multisets. 2. If I does not satisfy l j , 1 ≤ j ≤ k, then maxsat(φ) ≤ maxsat(φ l j ). Assume that there exists an assignment I of φ l j that falsifies less than maxsat(φ) clauses. If we extend I by assigning I (l j ) = true, we get an assignment of φ that falsifies less than maxsat(φ) clauses. But this is in contradiction with I being optimal. So, it holds that maxsat(φ) ≤ maxsat(φ l j ).

k + 1 sibling nodes below B labelled with φ l 1 , φ ¬l 1 ,l 2 , . . . , φ ¬l 1 ,...,¬l k-1 ,l k and φ ¬l 1 ,...,¬l k . This result can be proved with the same arguments of Lemmas 6.5 and 6.6. The extension of our approach to weighted MaxSAT/MinSAT and weighted partial MaxSAT/Min-SAT is as in branch-and-bound MaxSAT and MinSAT algorithms [START_REF] Abramé | On the resiliency of unit propagation to Max-Resolution[END_REF][START_REF] Li | New inference rules for max-SAT[END_REF][START_REF] Li | Optimizing with minimum satisfiability[END_REF]. Roughly speaking, in weighted MaxSAT/MinSAT, we just need to propagate weights, and given a multiset of empty weighted clauses {( , w 1 ), . . . , ( , w k )}, we replace it with {( , w 1 + • • • + w k )}. In weighted partial MaxSAT/MinSAT, we can apply the same inference as in SAT in the hard part.

Conclusions

We have defined three complete logical calculi for MaxSAT and MinSAT. The first calculus is valid for MaxSAT, the second is valid for MinSAT and the third is valid for both MaxSAT and MinSAT. One interesting aspect of these calculi is that they allow one to solve optimization instead of decision problems using logical tools and look at MaxSAT and MinSAT from a different angle.

As future work we plan to analyse how the proposed tableau calculi can be extended to nonclausal MaxSAT and MinSAT, as well as to deal with first-order logic formulas. We also plan to study how the calculi can be extended to many-valued logics. The results of this paper inspired a natural deduction MaxSAT calulus [START_REF] Casas-Roma | Solving MaxSAT with natural deduction[END_REF].

DEFINITION 4. 2

 2 Let φ = {C 1 , . . . , C m } be a multiset of clauses. A clause MaxSAT tableau for φ is constructed by a sequence of applications of the following expansion rules:Initialize A tree with a single branch with m nodes such that each node is labelled with a clause of φ is a clause MaxSAT tableau for φ. Such a tableau is called initial tableau, and its clauses are declared to be active. Extension Given a clause MaxSAT tableau T for φ, a branch B of T and a node of B labelled with an active clause l 1 ∨• • •∨l r with r ≥ 2, the tableau obtained by creating r sibling nodes below B and labelling each node with a different unit clause from {l 1 , . . . , l r } is a clause MaxSAT tableau for φ. The clause l 1 ∨ • • • ∨ l r becomes inactive in the new branches, and the unit clauses l 1 , . . . , l r are declared to be active. Contradiction Given a clause MaxSAT tableau T for φ, a branch B of T and two nodes of B labelled with two active unit clauses l and ¬l, the tableau obtained by appending a node labelled with an empty clause ( ) below B is a clause MaxSAT tableau for φ. The unit clauses l and ¬l become inactive in B, and the added empty clauses ( ) is considered active. DEFINITION 4.3

FIGURE 2 .

 2 FIGURE 2. Steps performed for saturating the leftmost branch of the completed clause MaxSAT tableau forφ = {¬x 1 , ¬x 2 , ¬x 3 , x 1 ∨ x 2 , x 1 ∨ x 3 , x 2 ∨ x 3 } from Example 4.7.

  The contradiction rule was applied on B: two complementary unit clauses in B become inactive and an empty clause is added to the new branch B . Since exactly one of the newly inactive unit clauses was falsified by I and we added one empty clause, I falsifies the same number of active clauses in B and B . • 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 B . The number of unsatisfied active clauses is preserved in B 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 unsatisfied active clauses is preserved in all these branches because C becomes inactive after the extension.

THEOREM 4. 6

 6 Completeness. Let φ be a multiset of clauses whose minimum number of clauses that can be falsified is m. Then, each completed clause MaxSAT tableau for φ has cost m.

  is an active clause of B, and I(x ) = 0 if variable x does not occur in any active 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 B whose active clauses form a multiset of unit clauses φ that contains as many unit clauses as clauses are in φ, and each literal of each unit clause of φ was derived from a different clause of φ. Since the clause of φ are unit and there are k complementary pairs of unit clauses, I satisfies |φ|k clauses of φ , 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.

FIGURE 4 .

 4 FIGURE 4. Completed clause MinSAT tableau for φ 1 = {¬x 1 , ¬x 2 , x 1 ∨ x 2 }.

FIGURE 5 .

 5 FIGURE 5. Completed clause MinSAT tableau forφ 2 = {x 1 ∨ x 2 , ¬x 1 ∨ x 3 , ¬x 2 ∨ ¬x 3 }.

FIGURE 6 .=

 6 FIGURE 6. Completed clause WMinSAT tableau for φ = {(x 1 , 1), (¬x 2 , 3), (x 1 ∨ ¬x 2 , 5), (x 1 ∨ ¬x 3 ; 2), (x 2 ∨ x 3 , 1)}.

FIGURE 7 .

 7 FIGURE 7. Proof tree for {¬x 1 , ¬x 1 , ¬x 2 , ¬x 2 , x 1 ∨ x 2 } using SAT clause branching.

TABLE 1 .

 1 Expansion rules of a complete clause tableau calculus for SAT which is WPMinSAT when all the soft clauses have the same weight; and MinSAT, which is PMinSAT without hard clauses. The SAT problem is PMaxSAT/PMinSAT without soft clauses.

  FIGURE 8. A completed clause MaxMinSAT tableau for {¬x 1 , ¬x 1 , ¬x 2 , ¬x 2 , x 1 ∨ x 2 }.DEFINITION 6.3Let T be a clause MaxMinSAT tableau for a multiset of clauses φ, and let B be a branch of T. Branch B is saturated iff its leaf node is labelled with the empty multiset or with a multiset of empty clauses.

∨ • • • ∨ l k }, the tableau obtained by appending k + 1 new left nodes below B labelled with the multisets φ l 1 , . . . , φ l k , φ ¬l 1 ,...,¬l k is a clause MaxMinSAT tableau for φ.

Downloaded from https://academic.oup.com/jigpal/advance-article-abstract/doi/10.1093/jigpal/jzz025/5544641 by guest on 18 February 2020

Acknowledgements

This work was supported by Project LOGISTAR from the EU H2020 Research and Innovation Programme under Grant Agreement No. 769142 and MINECO-FEDER projects RASO (TIN2015-71799-C2-1-P/2-P).

3. Finally, we have to prove that maxsat(φ) ≤ maxsat(φ ¬l 1 ,...,¬l k ). Observe that maxsat(φ ¬l 1 ,...,¬l k ) = maxsat(. . . (maxsat(maxsat(φ ¬l 1 ) ¬l 2 )...) ¬l k ). The literals ¬l i , 1 ≤ i ≤ k, which are satisfied by I preserve the number of unsatisfied clauses, and the literals ¬l j , 1 ≤ j ≤ k, which are not satisfied by I, can increase the number of unsatisfied clauses. Since I satisfies l 1 ∨ • (

PROOF. Let I be an optimal MinSAT assignment. We can prove, using the arguments of Lemma 6.5, that the maximum number of unsatisfied clauses in φ is the same as the maximum number of unsatisfied clauses in at least one of the multisets φ l 1 , . . . , φ l k , φ ¬l 1 ,...,¬l k and is not greater in the rest of multisets. We have to take into account the following facts: (i) if I satisfies a literal l i , 1 ≤ i ≤ k, then φ l i clearly preserves the number of unsatisfied clauses and so minsat(φ) = minsat(φ l i ). (ii) If I does not satisfy l j , 1 ≤ j ≤ k, then minsat(φ) ≥ minsat(φ l j ). Assume that there exists an assignment I of φ l j that falsifies more than minsat(φ) clauses. If we extend I by assigning I (l j ) = true, we get an assignment of φ that falsifies more than minsat(φ) clauses. But this is in contradiction with I being optimal. So, it holds that minsat(φ) ≥ minsat(φ l j ). THEOREM 6.7 A completed clause MaxMinSAT tableau for a multiset of clauses φ provides an optimal MaxSAT assignment and an optimal MinSAT assignment.

PROOF. The root node of a completed MaxMinSAT tableau is labelled with the input formula. Such a tableau is finite because each descendant has at least one variable less than its parents: at least one less variable in the descendants labelled with φ l 1 , . . . , φ l k and at least k less variables in the descendants labelled with φ ¬l 1 ,...,¬l k . Thus, after a finite number of steps, the leaves of a tableau contain either the empty formula or a multiset of empty clauses. By Lemma 6.5, all the branches with the minimum number of empty clauses correspond to optimal MaxSAT solutions. By Lemma 6.6, all the branches with the maximum number of empty clauses correspond to optimal MinSAT solutions. Besides, Lemmas 6.5 and 6.6 guarantee that the cost of each branch ranges between the maximum and minimum number of unsatisfied clauses in φ.

The clauses became empty because of the literals that were instantiated at each node that allowed to remove the complementary literals. Thus, in the optimal branches, the assignments that set those literals to true and the rest of literals appearing in the input formula to an arbitrary value are optimal assignments.

All the results of this section also hold if we replace the proposed extension rule with the following rule: if the leaf node of a branch B is labelled with the multiset φ = φ ∪ {l 1 ∨ • • • ∨ l k }, then append