Mohamed Sami Cherif
email: mohamedsami.cherif@lis-lab.fr

Djamal Habet
email: djamal.habet@lis-lab.fr

André Abramé
email: andre.abrame@logike.fr

Understanding the power of Max-SAT resolution through UP-resilience

Keywords: Branch and Bound, Max-SAT resolution, Simulated Unit Propagation, UP-resilience, Pattern

niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

The maximum satisfiability (Max-SAT) problem is an optimization extension of the satisfiability (SAT) problem. For a given formula in Conjunctive Normal Form (CNF), it consists in finding an assignment of the variables which maximizes the number of satisfied clauses. Complete methods for this problem include SAT based approaches (e.g. RC2 [START_REF] Alexey Ignatiev | RC2: an efficient maxsat solver, MaxSAT Evaluation[END_REF], MAXHS [START_REF] Davies | Solving maxsat by solving a sequence of simpler sat instances[END_REF], OPEN-WBO [START_REF] Martins | Open-wbo: A modular maxsat solver[END_REF], EVA [START_REF] Narodytska | Maximum satisfiability using core-guided maxsat resolution[END_REF], WPM1 [START_REF] Ansótegui | Solving (weighted) partial maxsat through satisfiability testing[END_REF]) and Branch and Bound (BnB) algorithms (e.g. AH-MAXSAT [START_REF] Abramé | ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver[END_REF], MiniMaxSAT [START_REF] Heras | MiniMaxSAT: An efficient weighted maxsat solver[END_REF], AKMAXSAT [START_REF] Küegel | Improved exact solver for the weighted max-sat problem[END_REF], MAXSATZ [START_REF] Li | Resolution-based lower bounds in maxsat[END_REF][START_REF] Li | Planes, New inference rules for max-sat[END_REF]) among others. The former which iteratively call SAT solvers are particularly efficient on industrial instances while the latter are competitive on random and crafted instances.

BnB based approaches construct a search tree and compute, at each node, the Lower Bound (LB) by counting the disjoint Inconsistent Subsets (ISs) of the formula using Simulated Unit Propagation (SUP) [START_REF] Li | Exploiting unit propagation to compute lower bounds in branch and bound max-sat solvers[END_REF]. When an IS is found, it is either temporarily deleted or transformed by Max-SAT resolution, the inference rule for Max-SAT [START_REF] Bonet | Resolution for max-sat[END_REF][START_REF] Heras | New inference rules for efficient Max-SAT solving[END_REF], to ensure that it will be counted only once.

However, learning Max-SAT resolution transformations, i.e., memorizing them in the current subtree (including the current node), may affect negatively the quality of the lower bound estimation [START_REF] Abramé | On the resiliency of unit propagation to maxresolution[END_REF][START_REF] Li | Planes, New inference rules for max-sat[END_REF][START_REF] Abramé | On the extension of learning for Max-SAT[END_REF]. Therefore, state of the art solvers learn transformations selectively mainly in the form of patterns [START_REF] Li | Planes, New inference rules for max-sat[END_REF].

Recently, new patterns called Unit Clause Subsets (UCSs) were introduced and empirically studied in [START_REF] Abramé | On the extension of learning for Max-SAT[END_REF]. The most significant feature of these patterns is producing unit clauses after the transformation by Max-SAT resolution. The propagation of these clauses may lead to the detection of more ISs. The empirical study of these patterns lead to the first observations on the relation between Max-SAT resolution transformations and the efficiency of the SUP mechanism which is indispensable for the lower bound estimation.

In this paper, we formally state these observations by introducing a new property called UP-resilience. More specifically, we study the impact of the Max-SAT resolution transformations on the SUP mechanism. We show that in some cases the information which can be used by SUP in the original formula are, after transformation, fragmented in several clauses. In such situation, SUP may be less efficient in the transformed formula than in the original one. We introduce the notion of UP-resilience to characterize the transformations which are not affected by fragmentation and more generally to measure the impact of the transformations on the SUP mechanism. We show that according to this criterion, the most used learning scheme based on patterns does not affect SUP. This contributes to explain from a theoretical point of view the empirical results obtained in the last ten years on the development of inference rules [START_REF] Li | Planes, New inference rules for max-sat[END_REF]. Also, in the context of a new approach to extend the current learning mechanisms, we conduct a theoretical study on particular UCS patterns and, more specifically, their relation with UP-resilience: we prove that binary UCSs are UP-resilient and we generalize this result on UCSs where only one clause of any size is involved in the conflict. Furthermore, we explain how our results can help extend the current patterns by showing that the current mechanisms in BnB solvers can't ensure UP-resilience for these patterns. Finally, we present empirical observations that also support the relevance of the UP-resilience property. This paper brings together, highlights and extends results presented in previous conference publications [START_REF] Abramé | On the resiliency of unit propagation to maxresolution[END_REF][START_REF] Cherif | Towards the characterization of max-resolution transformations of ucss by up-resilience[END_REF]. In particular, the notion of UP-resilience was first introduced and used to quantify the impact of Max-SAT resolution transformations on the SUP mechanism in [START_REF] Abramé | On the resiliency of unit propagation to maxresolution[END_REF]. Moreover, binary UCSs and UCSs patterns where only one clause of any size is involved in the conflict were proven to be UP-resilient in [START_REF] Cherif | Towards the characterization of max-resolution transformations of ucss by up-resilience[END_REF]. In this paper, we extend those results by showing that application orders can have a direct impact not only on the UP-resilience of certain literals appearing in the detected IS but also on the UP-resilience of the whole Max-SAT resolution transformation of the IS. Furthermore, we provide a proof for the UP-resilience of one of the major patterns, which does not correspond to a UCS, thus reinforcing our observations on the relevance of this property. We also provide more detailed experiments and new empirical results on partial instances. Finally, this paper includes a thorough background on Branch and Bound algorithms for Max-SAT and on the use of Max-SAT resolution in this context. This paper is organized as follows. In Section 2, we give basic definitions and notations and we present a brief overview of BnB solvers for Max-SAT.

In Section 3, we describe the fragmentation phenomenon as a motivation to our work. We introduce the notion of UP-resilience in Section 4 and we show how it highlights the impact of Max-SAT resolution transformations on the SUP mechanism. In Section 5, we conduct a theoretical study on particular UCS patterns and, more specifically, their relation with UP-resilience and we show the limits of the current mechanisms. In Section 6, we present empirical evidence on the relevance of UP-resilience. Finally, we conclude and we give some prospective points for future work in Section 7.

Preliminaries

Definitions and Notations

Let X be a set of propositional variables. A literal l is a variable x ∈ X or its negation x and a clause is disjunction of literals, represented as a set of literals.

A formula in Conjunctive Normal Form (CNF) is a conjunction of clauses and can be represented as a set of clauses. An assignment I : X -→ {true, f alse} maps each variable to a Boolean value and is represented as a set of literals. For a given literal l, var(l) denotes the variable appearing in l. A clause c is satisfied by an assignment I if at least one of its literals is satisfied, i.e., ∃l ∈ c such that An Inconsistent Subset (IS) of a formula Φ is an unsatisfiable set of clauses [START_REF] Niedermeier | New upper bounds for maximum satisfiability[END_REF]. Then, the value of LB is computed and compared to UB. If it is greater, finding a better solution in the current sub-tree is not possible and, thus, the algorithm backtracks. If a complete assignment is reached, the UB value is updated and a backtrack is performed. Else, an unassigned variable is chosen using a branching heuristic [START_REF] Abramé | ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver[END_REF][START_REF] Heras | MiniMaxSAT: An efficient weighted maxsat solver[END_REF][START_REF] Küegel | Improved exact solver for the weighted max-sat problem[END_REF][START_REF] Li | Resolution-based lower bounds in maxsat[END_REF]. These steps are repeated until the whole search space is explored. As the efficiency of BnB algorithms depends on the quality of LB, it is important to note that state of the art BnB Max-SAT solvers use powerful mechanisms to compute a more accurate LB estimation enabling more cuts in the search tree and, thus, faster solving.

ψ ⊆ Φ.

LB Estimation

The LB estimation is one of the most critical components of a BnB Max-SAT algorithm. Indeed, computing lower bounds with better quality entails more cuts in the search tree and, thus, faster solving. However, as these computations are done frequently during the search, the time devoted to them is closely correlated to the speed of the solver and, therefore, its efficiency. So, it is important to strike a balance between the computation time for LB and its quality. Inconsistent Subsets (ISs) in the simplified formula Φ| I , where I is the current assignment, using Simulated Unit Propagation (SUP) [START_REF] Li | Exploiting unit propagation to compute lower bounds in branch and bound max-sat solvers[END_REF].

SUP replicates the Unit Propagation (UP) mechanism, used in SAT solvers and which consists in iteratively satisfying the literals appearing in unit clauses until a conflict is found (an empty clause), to detect ISs. However, UP is not a valid inference rule for Max-SAT, i.e., it does not necessarily maintain the number of falsified clauses for each assignment. Thus, the variable assignments made by UP are not added to the current assignment after the LB estimation.

More specifically, these variable assignments are stored in a separate temporary assignment extension. That is why we say that BnB Max-SAT algorithms simulate UP and we refer to this mechanism as Simulated Unit Propagation.

The propagation steps generated by SUP can be represented by an implication graph [START_REF] Marques-Silva | Grasp: A search algorithm for propositional satisfiability[END_REF] defined as follows in the context of BnB solvers for Max-SAT:

Definition 1 (Implication Graph of an IS). Let ψ be an IS of a CNF formula Φ and I an assignment. We suppose that exactly one clause is falsified by I (SUP stopped when the first empty clause is generated). An implication graph of ψ is a directed acyclic graph G = (V, A) defined as follows: Notation. For an implication graph G and a literal l ∈ V (possibly ), we denote :

• V = {l ∈ I} ∪ { c | c ∈ ψ and |c| = 1} ∪ { } • A = {(l, l , c) | l, l ∈ I
• pred G (l) (resp. succ G (l)) the predecessors (resp. successors) of l in G • neigh G (l) = pred G (l) ∪ succ G (l)
• src G (l) the clause that lead to the propagation of the literal l in G

The index G will be omitted if there is no confusion.

When an IS is detected, it must be counted only once in the LB estimation.

To this end, detected ISs are treated using two methods: they are either temporarily deleted or transformed by Max-SAT resolution. The deletion of ISs has several advantages: it is less time-consuming and it doesn't increase the size of the formula. However, it produces a formula that is not equivalent to the original and, thus, that may contain less ISs. Therefore, this method applies local changes on the formula that are only preserved during the LB estimation in the current node. In the next section we explain the second method which transforms ISs using Max-SAT resolution.

Max-SAT resolution Transformation

The Definition 2 (Max-SAT resolution [START_REF] Bonet | Resolution for max-sat[END_REF][START_REF] Heras | New inference rules for efficient Max-SAT solving[END_REF]). The inference rule for Max-SAT, max-resolution, is defined as follows:

c = {x, y 1 , ..., y s }, c = {x, z 1 , ..., z t } cr = {y 1 , ..., y s , z 1 , ..., z t }, cc 1 , ..., cc t , cc t+1 , ..., cc t+s
where the compensation clauses are defined as follows:

cc 1 = {x, y 1 , ..., y s , z 1 } cc 2 = {x, y 1 , ..., y s , z 1 , z 2 } . . . cc t = {x, y 1 , ..., y s , z 1 , ..., z t-1 , z t } cc t+1 = {x, z 1 , ..., z t , y 1 } cc t+2 = {x, z 1 , ..., z t , y 1 , y 2 } . . . cc t+s = {x, z 1 , ..., z t , y 1 , ..., y 2 , y s }
Remark. Unlike the SAT inference rule, Max-SAT resolution replaces the premises in the rule by its conclusions. In addition, it produces an equivalent formula, i.e., it preserves the number of unsatisfied clauses for any assignment. The results established in this paper can be easily extended to weighted Max-SAT formulas (hard clauses can be included with infinite weights in the case of partial formulas) using the weighted version of Max-SAT resolution introduced in [START_REF] Bonet | Resolution for max-sat[END_REF].

Furthermore, as Max-SAT resolution is also a sound and complete inference rule for Min-SAT [START_REF] Li | An exact inference scheme for minsat[END_REF], our results remain valid in the context of B&B Min-Sat solvers.

Definition 3 (Max-SAT resolution transformation of an IS). Let ψ be an IS of a CNF formula Φ and S = x 1 , ..., x k be a sequence of variables appearing in ψ.

The Max-SAT resolution transformation of ψ with respect to S, denoted Θ(ψ, S), is the set of clauses obtained from ψ after the application of Max-SAT resolution steps in accordance to the sequence S, i.e., Θ(ψ, S) = θ(θ...(θ(ψ, x 1 ), x 2 )..., x k ) where θ(ψ, x) denotes the application of the Max-SAT resolution step on two clauses c and c such that x ∈ c and x ∈ c .

Remark. A transformation Θ(ψ, S) is not unique in general as the application of Max-SAT resolution steps with respect to a given variable sequence S is not deterministic and, thus, Θ(ψ, S) represents any of the possible outcomes after the transformation of ψ with respect to S. However, if S represents the reverse propagation order, the transformation with respect to S becomes deterministic and Θ(ψ, S) becomes unique. It is important to note that, unlike the deletion method, the changes are maintained in the sub-tree and, thus, the detected IS is computed and counted only once. This is possible since Max-SAT resolution produces an equivalent formula and this entails an incremental calculation of LB while reducing redundancy in the detection of ISs. Nevertheless, this method has several shortcomings: it is time-consuming and it may increase the size of the formula by adding the compensation clauses obtained after each Max-SAT resolution step. We explain in the next section how state of the art solvers overcome these limits.

x 1

x 2

x 4

x 3

{x 1 } { x 1 , x 2 , x 4 } {x 2 } { x1 , x2 , x4 } {x 3 } {x 3 , x 4 } { x 3 , x 4 } {x 1 , x 2 , x 4 } {x 3 , x 4 } {x 1 , x 2 , x 3 } {x 3 } {x 1 , x 2 } {x 2 } {x 1 } {x 1 } {x 1 , x 2 , x 3 , x 4 } {x 1 , x 3 , x 4 } {x 1 , x 2 , x 3 , x 4 } {x 1 , x 3 } {x 1 , x 2 , x 3 } {x 1 , x 2 } x 4
x 3

x 2

x 1 resolvents are smaller than four [START_REF] Heras | MiniMaxSAT: An efficient weighted maxsat solver[END_REF] whereas the second learns transformations matching particular patterns. These patterns are mainly described by inference rules that can be deduced from Max-SAT resolution. They can be specific cases of Max-SAT resolution or a combination of several Max-SAT resolution steps.

We give below three major patterns used in state of the art solvers:

{l 1 , l 2 }, {l 1 , l 2 } (P 1 ) {l 1 } {l 1 , l 2 }, {l 1 , l 3 }, {l 2 , l 3 } (P 2 ) {l 1 }, {l 1 , l 2 , l 3 }, {l 1 , l 2 , l 3 } {l 1 }, {l 1 , l 2 }, {l 2 , l 3 }, ..., {l k , l k+1 }, {l k+1 } (P 3 ) , {l 1 , l 2 }, {l 2 , l 3 }, ..., {l k , l k+1 }
P 1 is a particular case of Rule 1 in [START_REF] Li | Planes, New inference rules for max-sat[END_REF] while P 2 is related to Rule 5 and P 3 corresponds to Rule 4. In their weighted form, the pattern (P 1 ) corresponds to a particular case of chain resolution rule [START_REF] Larrosa | A logical approach to efficient Max-SAT solving[END_REF] whereas patterns (P 2) and (P 3) are specific cases of the cycle resolution rule [START_REF] Larrosa | A logical approach to efficient Max-SAT solving[END_REF]. A pattern can cover an IS entirely as in pattern (P 3), or partially as in patterns (P 1) and (P 2). These patterns present several advantages: they can be easily identified and they don't increase the number of clauses in the formula. Furthermore, patterns (P 1) and (P 2) produce a unit resolvent clause which enables the solver to detect more ISs using SUP.

Recently, new patterns called Unit Clause Subsets (UCS) [START_REF] Abramé | On the extension of learning for Max-SAT[END_REF], were introduced and empirically studied in order to extend the learning mechanisms in BnB Max-SAT solvers. Hereafter, we give the formal definition of these patterns and we explain how they can be easily detected using the implication graph of an IS. Definition 5 (First Unique Implication Point [START_REF] Zhang | Efficient conflict driven learning in a boolean satisfiability solver[END_REF]). Let G be an implication graph. A Unique Implication Point (UIP) is any node in G such that any path from the literals propagated by unit clauses to the conflict node must pass through it. The First UIP (FUIP) is the UIP closest to the conflict node.

UCS patterns have a high apparition frequency (in more than 57% of the detected ISs [START_REF] Abramé | On the extension of learning for Max-SAT[END_REF]). Furthermore, certain k-UCS patterns are easily detectable by analyzing the implication graph of the obtained IS. Indeed, as outlined in Example 3, the clauses which are between the conflict and the FUIP produce a unit resolvent clause if they are transformed by Max-SAT resolution in the reverse propagation order.

Example 3. We consider the IS ψ = {{x 1 }, {x 2 }, {x 1 , x 2 , x 3 }, {x 3 , x 4 }, {x 3 , x 5 }, {x 4 , x 5 }} detected by the sequence of unit propagations represented in the form of the implication graph G on the left in Figure 2. Clearly, the node x 3 is the FUIP of G. The Max-SAT resolution transformation of ψ with respect to the variable sequence S = x 5 , x 4 , x 3 (representing the reverse order of propagation until the FUIP is encountered) is given on the right in Figure 2. This transformation produces the unit resolvent {x 3 }. Therefore, the set of clauses

ψ = {{x 3 , x 4 }, {x 3 , x 5 }, {x 4 , x 5 }} ⊂ ψ is a 3-UCS. More specifically, since all the clauses in ψ are binary, it is a 3 b -UCS. x 1 x 2 x 3 x 4 x 5 {x 1 } { x 1 , x 2 , x 3 } {x 2 } { x1 , x2 , x3 } { x 3 , x 4 } { x 3 , x 5 } { x 4 , x 5 } { x 4 , x 5 } {x 4 , x 5 } {x 3 , x 5 } {x 3 , x 4 } {x 3 , x 4 } {x 3 } {x 3 , x 4 , x 5 } {x 3 , x 4 , x 5 } x 5 x 4

Motivation

Two reasons are generally invoked to explain the efficiency of the learning schemes: they limit the growing of the formula size and produce small compensation clauses which are more likely to be used by SUP. However, experimental analysis shows that increasing learning slightly may deteriorate significantly the performance of the solver [START_REF] Abramé | On the extension of learning for Max-SAT[END_REF]. The reasons cited above cannot explain this behavior. Furthermore, the empirical study conducted in [START_REF] Abramé | On the extension of learning for Max-SAT[END_REF] shows a correlation between the decrease of the number of propagations, the decrease of the number

| {x4} = {{x 1 , x 3 }, {x 1 , x 3 }, {x 1 , x 2 }, {x 1 , x 2 , x 3 }, {x 1 , x 2 , x 3 }, }. Clearly, the literal x 1 can't be propagated in Θ(ψ, S)| {x4} .
We can produce the resolvent x 1 if we perform a Max-SAT resolution step between the clauses {x 1 , x 3 } and {x 1 , x 3 } but the SUP mechanism alone cannot ensure the propagation of this literal in the transformed IS even with respect to its neighborhood in the implication graph. We say that the information leading to the propagation of x 1 was fragmented into several compensation clauses.

When such transformations are learned, it may affect the capability of the SUP mechanism to detect ISs in the lower nodes of the search tree. Thus, the LB estimation may be less accurate and the solvers may explore more nodes.

A New Characterization of Max-SAT resolution Transformations

In this section, we introduce the notion of UP-resilience of a transformation and we explain how this property quantifies the impact of Max-SAT resolution on the SUP mechanism and, thus, on the detection of Inconsistent Subsets. We also prove that the main patterns (P1), (P2) and (P3) used in state-of-theart BnB solvers for Max-SAT verify this property. Finally, we show that the application order of Max-SAT resolution has an impact on the UP-resilience of a transformation.

UP-Resilience

When fragmentation occurs, the compensation clauses which may propagate a literal of the constructed implication graph can contain additional literals which are not in its initial neighborhood. More precisely, the neighborhood of a literal l in the implication graph contain literals that are in direct interaction with it and which should enable, once propagated in the detected IS, the propagation of l. However, if after the transformation of the IS, the fragmentation occurs, new literals that interact directly with l are introduced and may thus obstruct the propagation of l by SUP even considering all the literals appearing in its neighborhood in the implication graph. Clearly, the power of SUP is depleted in such cases. Thus, to detect if a transformation is not affected by the fragmentation phenomenon, we can rely on the capability of SUP to propagate the literals of the constructed implication graph when their neighborhood literals are set to true. From here on, we will say that a literal l can be propagated in a formula Φ if the unit clause {l} can be inferred from Φ by unit propagation.

Definition 6 (UP-Resilience in an Implication Graph). Let Φ be a CNF formula, ψ an IS detected by the propagation steps described by the implication graph G = (V, A) and S a sequence of variables appearing in ψ. We say that the transformation Θ(ψ, S) is UP-resilient for l ∈ V in G iff ∈ neigh(l) or l can be propagated in Θ(ψ, S)| neigh(l) . We say that Θ(ψ, S) is UP-resilient for

L ⊆ V in G iff it is UP-resilient ∀l ∈ L in G and that it is UP-resilient in G iff it is UP-resilient for V in G.
Remark. Note that the neighborhoods which include the special node are not valid assignments. All transformations are considered UP-resilient for literals with such neighborhoods. x 1

x 2

x 4

x 3 In the previous definition, the UP-resilience of a transformation may therefore vary depending on how the IS has been detected since it depends on the constructed implication graph. To overcome this limitation, we propose to consider all the possible ways (i.e. sequences of propagation steps) to detect the IS. To this end, we introduce the set of the possible neighborhoods of a literal appearing in an IS.

{x 1 } { x 1 , x 2 , x 4 } {x 2 } { x1 , x2 , x4 } {x 3 } {x 3 , x 4 } { x 3 , x 4 } x 1 x 2 x 3 x 4 {x 1 } { x 1 , x 2 , x 4 } {x 2 } {x 1 , x 2 , x 4 } {x 3 } {x 3 , x 4 } { x 1 , x 2 , x 4 }
Definition 7 (Possible Neighborhoods). Let Φ be a CNF formula and ψ an IS of Φ. For a literal l appearing in ψ, we define its possible neighborhoods as

pneigh(l) = {neigh G (l)|G = (V, A) implication graph of ψ s.t. l ∈ V }.
We extend this definition on any set of literals L appearing in ψ as pneigh(L) =

{ l∈L neigh G (l)|G = (V, A) implication graph of ψ s.t. L ⊆ V }.
Next, we can give a general definition of UP-resilience which does not depend anymore on the propagation steps which have led to the IS discovery.

can't be propagated in Θ(ψ, S)| N = {{x 1 , x 3 }, {x 1 , x 3 }, {x 1 , x 2 }, {x 1 , x 2 , x 3 }, {x 1 , x 2 , x 3 }, }.
Therefore, the transformation is not UP-resilient for x 1 and, consequently, it is not UP-resilient.

Similarly, we can further quantify the impact of a Max-SAT resolution transformation of an IS ψ on SUP by considering its percentage of UP-resilience, i.e, the percentage of couples (l, N ) s.t. ∈ N or l can be propagated in Θ(ψ, S)| N .

Finally, notice that in the case of (weighted) partial formulas, the presence of hard clauses may have a direct impact on the UP-resilience of the detected ISs.

Indeed, as hard clauses are maintained after the application of weighted Max-SAT resolution, a literal propagated by a hard clause can always be propagated with respect to its neighborhood in the corresponding implication graph after the transformation of the IS.

Impact on IS Detection

One of the most interesting properties of UP-resilient transformations is the capability to retrieve the propagations which are not necessary anymore to an IS. We have seen that if a transformation is UP-resilient for a literal l, then l can be propagated in the transformed formula when the literals of each possible neighborhood, not containing the empty clause, are set to true. We now show that this property can be extended to sets of literals, i.e., if a transformation is UP-resilient for a set of literals L, then the literals of L can be propagated in the transformed formula with respect to the possible neighborhoods of L, not containing the empty clause. This is stated more formally in the following property:

Property 1. Let Φ be a CNF formula, ψ an IS of Φ and S a sequence of variables appearing in ψ. For any set of literals L appearing in ψ, if the trans-

formation Θ(ψ, S) is UP-resilient for L then ∀N ∈ pneigh(L) : ∈ N or ∀l ∈ L, l can be propagated in Θ(ψ, S)| N \{l} .
Proof. We prove this property by induction on |L| = n:

• If n = 1, then L = {l} and the property is verified.

• Suppose the property is true for every set of size n. Let L be of size n + 1 and l a literal in L. We set L = L \ {l} and let N ∈ pneigh(L). Clearly, Thus, We have the following cases: We deduce that ∀N ∈ pneigh(L) :

N = N 1 ∪ N 2 where N 1 ∈ pneigh(L ) and N 2 ∈ pneigh(l).
-If ∈ N 1 or ∈ N 2 then ∈ N -Else,
∈ N or every literal l in L can be propagated in Θ(ψ, S)| N \{l} .

When a subset ψ of an IS ψ is not necessary anymore (for instance when ψ is not minimal), this property ensures that SUP can perform the same propagations in the transformed formula as in the original clauses of ψ . More specifically, the UP-resilience of a set of literals L with respect to its neighborhood neigh(L) is maintained individually on every literal in L.

UP-Resilience of Main Patterns

Empirical results have shown that the existing learning schemes are efficient, but until now there was no theoretical explanation to these experimental facts.

Hereafter, we show that the main patterns (P 1), (P 2) and (P 3) used in state of the BnB solvers for Max-SAT are UP-resilient which contributes to explain theoretically the efficiency of these patterns.

Proposition 1. Let Φ be a CNF formula, ψ an IS and ψ ⊂ ψ such that ψ matches the premises of pattern (P 1 ). Then, the Max-SAT resolution transformation described in (P 1 ) is UP-resilient.

Proof. ψ = {{l 1 , l 2 }, {l 1 , l 2 }}. Therefore, there are two possible propagation sequences whose implication graphs are represented in Figure 4. Since all possible neighborhoods of literals l 1 , l 2 and l 2 contain the empty clause, the transformation of ψ as in (P 1 ) with respect to the only possible variable sequence Proposition 2. Let Φ be a CNF formula, ψ an IS and ψ ⊂ ψ such that ψ matches the premises of pattern (P 2 ). Then, the Max-SAT resolution transformation described in (P 2 ) is UP-resilient.

S = < var(l 2 ) > is UP-resilient. l 1 l 2 {l 1 , l 2 } {l 1 , l 2 } {l 1 , l 2 } l 1 l 2 {l 1 , l 2 } {l 1 , l 2 } {l 1 , l 2 }
Proof. ψ = {{l 1 , l 2 }, {l 1 , l 3 }, {l 2 , l 3 }}. Therefore, there are two possible propagation sequences whose implication graphs are represented in Figure 5. There are two Max-SAT resolution application orders S 1 = < var(l 2 ), var(l 3 ) > and S 2 = < var(l 3 ), var(l 2 ) > that produce the same transformation described by pattern (P 2 ). Since all possible neighborhoods of l 2 and l 2 contain the empty clause, the transformation of ψ by Max-SAT resolution is UP-resilient for l 2 and l 2 . We have pneigh(l 1 ) = {{l 3 , } ∪ pred(l 1 ), {l 2 , l 3 } ∪ pred(l 1 )}, where pred(l 1 )) denotes the predecessors of l 1 , and clearly the clause c = {l 1 , l 2 , l 3 }

propagates l 1 when the literals l 2 , l 3 in its second neighborhood are set to true.

Also, pneigh(l 3 ) = {{l 1 , }, {l 1 , l 2 }} and similarly the clause c = {l 1 , l 2 , l 3 } propagates l 3 when the literals in its neighborhood {l 1 , l 2 } are set to true. Proposition 3. Let Φ be a CNF formula, ψ an IS that matches the premises of pattern (P 3 ). Then, the Max-SAT resolution transformation described in (P 3 )

l 1 l 3 l 2 {l 1 , l 3 } {l 2 , l 3 } {l 1 , l 2 } {l 1 , l 2 } l 1 l 3 l 2 { l1 , l3 } { l 1 , l 2 } { l 2 , l 3 } { l2 , l3 }
is UP-resilient.

Proof. ψ = {{l 1 }, {l 1 , l 2 }, {l 2 , l 3 }, ..., {l k , l k+1 }, {l k+1 }}. Therefore, there are k possible propagation sequences whose implication graphs are represented in Figure 6. In each graph a different clause of ψ, containing the literal l i where

1 < i < k +1 is falsified. When i = 1 (resp. i = k +1), the unit clause {l i } (resp. {l k+1 }) is falsified. We have pneigh(l i ) = {{l i-1 , l i+1 }, {l i-1 , }} for 1 < i < k
and, clearly, the clause {l i , l i+1 }, obtained after the transformation, ensures the propagation of the literal l i with respect to its neighborhood {l i-1 , l i+1 }.

Also, for literals l 1 and l k+1 , we have respectively pneigh(l 1 ) = {{l 2 }, { }} and pneigh(l k+1 ) = {{l k , }} and, clearly, the clause {l 1 , l 2 } ensures the propagation of the literal l 1 with respect to its neighborhood {l 2 }. The same arguments ensure UP-resilience for literals l i for

1 ≤ i ≤ k + 1.
It is important to note that this proof on the UP-resilience of ISs matching the premises of pattern (P 3)

is clearly valid for every Max-SAT resolution application order consistent with

(P 3). l 1 l k+1 ... ... l i-1 l i {l 1 } {l k+1 } {l 1 , l 2 } {l k , l k+1 } {l i-2 , l i-1 } {l i , l i+1 } { l i -1 , l i } { li -1 , li }

UP-Resilience and Max-SAT resolution Application Orders

An important factor that has a direct impact on the UP-resilience property is the Max-SAT resolution application order. Two orders are used in BnB solvers for Max-SAT:

• The Reverse Propagation Order (RPO): applies Max-SAT resolution steps in the reverse order of propagation and is used in most state of the art solvers.

• The Smallest Intermediary Resolvent (SIR) [START_REF] Abramé | Efficient application of max-sat resolution on inconsistent subsets[END_REF] applies the Max-SAT resolution steps according to the size of the resolvents between clauses, favoring the smallest ones.

In Example 8, we show that application orders can have a direct impact not only on the UP-resilience of certain literals appearing in the detected IS, but also on the UP-resilience of the Max-SAT resolution transformation of the IS.

Furthermore, we empirically evaluate the impact of the current orders of application of Max-SAT resolution on the UP-resilience of the transformation in Section 6.

Example 8. We consider the IS ψ = {{x 1 }, {x 2 }, {x 3 }, {x 3 , x 4 }, {x 1 , x 2 , x 4 }}, introduced in Example 1, whose distinct implication graphs corresponding to the possible propagation sequences are represented in Figure 3. In Example 7, we showed that the transformation of ψ with respect to PRO is not UP-resilient since, in particular, it is not UP-resilient for literal x 1 . Now, we consider the Max-SAT resolution transformation of ψ with respect to the variable sequence S = x 3 , x 4 , x 1 , x 2 corresponding to SIR which is given in Figure 7. We have Therefore, the transformation Θ(ψ, S) is UP-resilient.

Θ(ψ, S) = {{x 1 , x 2 }, {x 1 , x 4 }, {x 3 , x 4 }, {x 1 , x 2 ,
In the next section, we characterize the Max-SAT resolution transformations of UCS patterns by UP-resilience. In particular, we introduce new Max-SAT resolution application orders that ensure the UP-resilience of UCS patterns and we also show that the current orders can't ensure UP-resilience for these patterns.

{x 3 } {x 3 , x 4 } {x 4 } {x 1 , x 2 , x 4 } {x 1 , x 2 } {x 1 } {x 2 } {x 2 } {x 3 , x 4 } {x 1 , x 4 } {x 1 , x 2 , x 4 } {x 1 , x 2 } x 3 x 4
x 1

x 2

On the UP-Resilience of UCSs

In this section, we prove that binary k-UCSs are UP-resilient by providing two different orders that ensure the UP-resilience of their transformation by Max-SAT resolution. We also show that unlike the given orders, the current used mechanisms can't ensure UP-resilience for these patterns which provides an explanation to the empirical results in [START_REF] Abramé | On the extension of learning for Max-SAT[END_REF] and shows that our results can help extend the current used patterns in state of the art solvers. Furthermore, we generalize our result on the resilience of k b -UCSs to k-UCSs where all clauses are binary except one of any size that is involved in the conflict.

Implication Graphs of UCS Patterns

In this section, we establish a characterization of implication graphs of the Proof. Since l is a UIP, all the paths from the literals propagated by unit clauses to the conflict node in G pass through it. We have |succ(l)| = s. Therefore, there are at least s different paths from l to in G. Let p 1 ,...,p s be those paths.

Suppose we have a different path p s+1 from l to . We have two possible cases:

• |pred( )| = s. This is absurd since the conflict clause is of size s and thus |pred( )| = s.

• Else, since |pred( )| = s, there exists l = l ∈ p s+1 and i ∈ {1, ..., s} such that l ∈ p i and |pred(l )| > 1. This is absurd since all clauses of ψ except the conflict clause are binary.

We deduce that there are exactly s different paths from l to in G. The same argument of the second case ensures that these paths are disjoint.

As explained in Section 2.2.4, when a UCS is detected, we know that the reverse propagation order ensures the production of a unit resolvent clause after the transformation. However, in general, this is not necessarily true for all application orders. Since this is the main feature of UCS patterns, we must ensure that the introduced orders produce a unit resolvent clause. It is important to note that the condition on the successors of the FUIP in Lemma 1 ensures the production of such clause for all possible orders. In the next section, we prove the UP-resilience of binary k-UCSs. To this end, we show in the next proposition that the condition on the FUIP successors in Lemma 1 is always verified for binary k-UCSs. Later, when we generalize our result, we only consider the graphs described by Lemma 1, i.e., which verify the condition on the successors of the FUIP. Proof. Suppose that |succ(l)| = 2. We have two possible cases:

• if |succ(l)| > 2 then, since |succ( )| = 2, there exists a literal with two predecessors. This is absurd since all the clauses are binary.

• if |succ(l)| = 1 then l is not the FUIP which is absurd.

On the UP-Resilience of Binary UCSs

In Section 4.3, we proved the UP-resilience of the main patterns. The next corollary is an immediate consequence of this result:

Corollary 1. For k ∈ {2, 3}, k b -UCSs are UP-resilient.
Proof. 2 b -UCSs and 3 b -UCSs are all of the respective forms

ψ 2 b = {{l 1 , l 2 }, {l 1 , l 2 }}
and ψ 3 b = {{l 1 , l 2 }, {l 1 , l 3 }, {l 2 , l 3 }} which correspond to the premises of patterns (P 1 ) and (P 2 ). Thus, we obtain the wanted result using Propositions 1 and 2.

In this section, we want to generalize the result of Corollary 1 to all binary k-UCSs. To this end, we introduce new orders of application of Max-SAT resolution using the characterization established in Lemma 1. We prove the resilience of k b -UCSs with respect to these orders and we explain theoretically the inefficiency of the current orders for these patterns.

Definition 9 (Path Resolvent Order). Let p 1 = l, l p1 1 , ..., l p1 n1 , (n 1 ≥ 0) and p 2 = l, l p2 1 , ..., l p2 n2 , (n 2 ≥ 0) denote two disjoint paths from l to . The Path Resolvent Order (PRO) of p 1 and p 2 is defined as P RO(p 1 , p 2 ) = var(l p1 1 ), ..., var(l p1 n1 ), var(l p2 1 ), ..., var(l p2 n2 ) .

Theorem 1. For any k ≥ 2, the transformation of k b -UCSs with respect to PRO is UP-resilient.

Proof. Let k ≥ 2 and ψ be a k b -UCS recognized by the FUIP l in the implication graph G of an IS. By Lemma 1 and Proposition 4, we know that there are 2 disjoint paths from l to in G. Let p 1 = l, l p1 1 , ..., l p1 n1 , (n 1 ≥ 0) and p 2 = l, l p2 1 , ..., l p2 n2 , (n 2 ≥ 0) denote these paths in G where n 1 + n 2 = k -1. And, suppose w.l.o.g that l p1 n1 = l is the conflict literal, i.e., the last propagated literal. We have two possible propagation sequences whose implication graphs are G and G represented in Figure 8. We prove that the Max-SAT resolution transformation relatively to the order

O = P RO(p 1 , p 2 ) is UP-resilient:
• The clause propagating l is not deleted after the transformation by Max-SAT resolution relatively to the order O so it clearly propagates l if its predecessors are set to true and thus the transformation by Max-SAT resolution relatively to the order O is UP-resilient for l. This argument also applies for the literals that were involved in the propagation of l.

• All possible neighborhoods of literals l p1 n1 = l and l contain the empty clause. Therefore, the transformation by Max-SAT resolution relatively to the order O is UP-resilient for l and l .

• For i ∈ {1, 2}, we set l pi 0 = l. Every literal l pi j such that 1 ≤ j < n i admits exactly one neighborhood neigh(l p1 j ) = {l pi j-1 , l pi j+1 } that doesn't contain the empty clause. Similarly, for l p2 n2 , we have neigh(l p2 n2 ) = {l pi n2-1 , l }. The Max-SAT resolution step on var(l p1 j )(1 ≤ j < n i ) is of the form:

{l, l pi j }, {l pi j , l pi j+1 } {l, l pi j+1 }, {l, l pi j , l pi j+1 }, {l, l pi j , l pi j+1 }

The clause c = {l, l pi j , l pi j+1 } clearly ensures the propagation of literal l pi j+1 if l pi j ∈ neigh(l pi j+1 ) is set to true since l is propagated by the unit resolvent clause {l}. Also, for j = 1, the clause c = {l, l p1 1 , l p1 2 } ensures the propagation of l p1 1 if l, l p1 2 ∈ neigh(l p1 1 ) are set to true. Thus, We deduce that the transformation is UP-resilient for l pi j where 1 ≤ j ≤ n i (j = n 1 ).

We conclude that the transformation of ψ by Max-SAT resolution relatively to the order O is UP-resilient.

Definition 10 (Path Resolvent Circular Order). Let p 1 = l, l p1 1 , ..., l p1 n1 , (n 1 ≥ 0) and p 2 = l, l p2 1 , ..., l p2 n2 , (n 2 ≥ 0) denote two disjoint paths from l to . The Path Resolvent Circular Order (PRCO) of p 1 and p 2 is defined as

P RCO(p 1 , p 2 ) = var(l p1
1 ), ..., var(l p1 n1 ), var(l p2 n2 ), ..., var(l p2 1 ) .

Theorem 2. For any k ≥ 2, the transformation of k b -UCSs with respect to PRCO is UP-resilient.

Proof. Let k ≥ 2 and ψ be a k b -UCS recognized by the FUIP l in the implication graph G of an IS. By Lemma 1 and Proposition 4, let p 1 = l, l p1 1 , ..., l p1 n1 , (n 1 ≥ 0) and p 2 = l, l p2 1 , ..., l p2 n2 , (n 2 ≥ 0) denote the two disjoint paths from l to in G where n 1 + n 2 = k -1. And, suppose w.l.o.g that l p1 n1 = l is the conflict literal. We have two possible propagation sequences whose implication graphs are G and G represented in Figure 8. We prove that the Max-SAT resolution transformation relatively to the order O = P RCO(p 1 , p 2 ) is UP-resilient:

• The same arguments in the proof of Theorem 1 ensure the UP-resilience of the transformation respectively to O for l p1 j (1 ≤ j ≤ n 1 ) and l as well as l and all the literals involved in its propagation.

• Every literal l p2 j such that 1 ≤ j ≤ n 2 admits exactly one neighborhood neigh(l p2 j ) = {l p2 j-1 , l p2 j+1 } that doesn't contain the empty clause (we set l p2 0 = l and l p2 n2+1 = l ). The Max-SAT resolution step on var(l p2 j ) (j = 1) is of the form: {l, l p2 j }, {l p2 j , l p2 j-1 } {l, l p2 j-1 }, {l, l p2 j , l p2 j-1 }, {l, l p2 j , l p2 j-1 }

The clause c = {l, l p2 j , l p2 j-1 } clearly ensures the propagation of literal l p2 j when l p2 j-1 ∈ neigh(l p2 j ) is set to true since l is propagated by the unit resolvent clause {l}. Also, the clause c = {l, l p2 2 , l p2 1 }, generated by the Max-SAT resolution step on var(l p2

2 ), clearly ensures the propagation of l p2 1 when its neighbors l, l p2 2 ∈ neigh(l p2 1 ) are set to true. Thus, the transformation is UP-resilient for l p2 j where 1 ≤ j ≤ n 2 .

We conclude that the transformation by Max-SAT resolution relatively to the order O is UP-resilient.

There is a major difference between the orders we introduced. Indeed, PRCO ensures a linear input resolution transformation, i.e., at each intermediary Max-SAT resolution step we use the resolvent obtained in the previous step and a clause from the detected k b -UCS. This is not always the case for PRO. The following result is an immediate consequence of either Theorem 1 or 2.

Corollary 2. For any k ≥ 2, k b -UCSs are UP-resilient.

Empirical results show that 2 b -UCSs and 3 b -UCSs, which correspond respectively to the patterns (P 1) and (P 2) have a positive impact on the performance of BnB solvers for Max-SAT [START_REF] Abramé | On the extension of learning for Max-SAT[END_REF][START_REF] Li | Resolution-based lower bounds in maxsat[END_REF]. The result in corollary 1 obtained through properties 1 and 2 prove that 2 b -UCSs and 3 b -UCSs are UP-resilient for any given order of application of Max-SAT resolution which explains why learning them has a positive impact regardless of the chosen order. This is not the case for k b -UCSs when k > 3. Empirical studies on the AHMAXSAT solver in [START_REF] Abramé | On the extension of learning for Max-SAT[END_REF] show that learning 4 b -UCSs and 5 b -UCSs has a major negative impact on its performance. This can be explained by the inadequacy of the Max-SAT resolution application orders used in state of the art BnB solvers for k b -UCSs when k > 3. More specifically, the SIR heuristic becomes practically unusable since all the intermediary resolvents have the same size (binary) as shown in the proofs of Theorems 1 and 2, whereas the Reverse Propagation Order doesn't always ensure the UP-resilience of the transformation as shown in the following example on a 4 b -UCS which can be easily extended to any k b -UCS for k > 4.

Example 9. We consider the IS ψ = {{l}, {l, l 1 }, {l, l 2 }, {l 1 , l 3 }, {l 2 , l 3 }} detected by one of the possible implication graphs represented on the left in Figure 9 after the respective propagation of literals l 1 , l 2 and l 3 (or l 3 ). Clearly, the

subset ψ = {{l, l 1 }, {l, l 2 }, {l 1 , l 3 }, {l 2 , l 3 }} ⊂ ψ is a 4 b -UCS recognized by the FUIP l.
The Max-SAT resolution transformation of ψ with respect to RPO which corresponds to the variable sequence S = var(l 3 ), var(l 2 ), var(l 1 ) is represented on the right in Figure 9.

l l 1 l 3 l 2 {l} {l, l 1 } {l 1 , l 3 } { l , l 2 } { l2 , l3 } {l 2 , l 3 } l l 2 l 3 l 1 {l} {l, l 2 } {l 2 , l 3 } { l , l1 } { l 1 , l 3 } {l 1 , l 3 } {l 2 , l 3 } {l 1 , l 3 } {l 1 , l 2 } {l, l 2 } {l, l 1 } {l, l 1 } {l} {l 1 , l 2 , l 3 } {l 1 , l 2 , l 3 } {l, l 1 , l 2 } {l, l 1 , l 2 } var(l 3 ) var(l 2 )
var(l 1 ) The literal l 1 has one neighborhood neigh(l 1 ) = {l, l 3 } that doesn't contain the empty clause. Clearly, the literal l 1 can't be propagated in

Θ(ψ, S)| neigh(l1) = {{l 1 , l 2 }, {l 1 , l 2 }}.
Similarly, the fragmentation phenomenon also occurs for l 2 and we conclude that the transformation of ψ relatively to RPO is not UPresilient.

Generalization to UCSs

In this section, we generalize our result to k-UCSs where all clauses are binary except one of any size that is involved in the conflict when the implication graph corresponds to the characterization established in Lemma 1. A clause involved in the conflict is either the falsified clause or contains the conflict literal, i.e., the last propagated literal. Unfortunately, although PRCO has the advantage of ensuring a linear input transformation, we couldn't generalize it to obtain the wanted result. Nevertheless, we managed to prove our result using a generalization of PRO to a multitude of paths.

Definition 11 (Multiple Path Resolvent Order). Let s ≥ 2 and p 1 = l, l p1 1 , ..., l p1 n1 , , ..., p s = l, l p2 1 , ..., l ps ns , denote s disjoint paths from l to .

The Multiple Path Resolvent Order (MPRO) of p 1 , ..., p s is defined inductively on s as follows:

-

If s = 2, M P RO(p 1 , p 2 ) = P RO(p 1 , p 2 )
-Else M P RO(p 1 , ..., p s ) = P RO( l, M P RO(p 1 , ..., p s-1 ), , p s ). Proof. We suppose w.l.o.g that c = {l 1 , ..., l s }. By Lemma 1, there are exactly s disjoint paths p 1 = l, l p1 1 , ..., l p1 n1 , , ..., p s = l, l ps 1 , ..., l ps ns , from l to in the implication graph G, represented in Figure 10, such that s i=1 n i = k -1 and l pi ni = l i for i ∈ {1, ..., s}. Other than G, there are exactly s-1 s = s possible implication graphs all similar to the graph G represented in Figure 10. We conclude that the transformation by Max-SAT resolution relatively to the order O is UP-resilient.

l p1 n1 = l 1 l p2 n2 = l 2 . . . l ps ns = l s c c c l l p2 1 l p1 1 ... l ps-1 1 l ps 1 ... ... l p1 n1 = l 1 l p2 n2 = l 2 . . . ...
{l, l 1 , l 2 , l 3 } {l, l 1 } {l, l 2 , l 3 } {l, l 2 } {l, l 3 } {l, l 3 } {l} {l, l 1 , l 2 } {l, l 1 , l 2 , l 3 } {l, l 2 , l 3 } var(l 1 )
var(l 2 ) The SIR order is defined relatively to the size of the intermediary resolvents.

var(l 3 ) {l, l 1 , ..., l s+1 } {l, l 1 } {l, l 2 , ..., l s+1 } {l, l 2 } cc 1 = {l, l 1 , l 2 } . . . cc s = {l, l 1 , l 2 , ..., l s , l s+1 } . . . var(l 1 )
Thus, it may theoretically simulate any order when the sizes of the resolvents are the same or many different orders when many resolvents share the same size which is the case of the studied UCSs. That's why this heuristic remains practically unusable even in the generalized case. Furthermore, RPO doesn't necessarily ensure the UP-resilience of k-UCSs described in the previous corollary. We finish this section by an example that highlights this fact. This example where the non binary clause is tertiary can be easily extended to any size s > 3. {{l}, {l, l 2 }, {l 2 , l 4 }, {l 2 , l 4 }}. We conclude that the transformation of ψ relatively to RPO is not UP-resilient.

l l 1 l 4 l 2 l 3 {l} {l, l 1 } {l 1 , l 4 } { l , l 2 } { l , l3 } c c c l l 1 l 4 l 2 l 3 {l} {l, l 1 } {l 1 , l 4 } { l, l 2 } { l , l 3 } c {l, l 3 } c {l 1 , l 4 } {l 2 , l 3 , l 4 } {l 1 , l 2 , l 3 } {l, l 3 } {l, l 1 , l 2 } {l, l 2 } {l, l 1 } {l, l 1 } {l} {l 1 , l 2 , l 3 , l 4 } {l 1 , l 2 , l 4 } {l 1 , l 2 , l 3 , l 4 } {l, l 1 , l 2 , l 3 } {l, l 1 , l 3 } {l, l 1 , l 2 , l 3 } {l, l 1 , l 2 } var(l 4 ) var(l 3 ) var(l 2 )
var(l 1 )

Empirical Study on the Relevance of UP-Resilience

In this section, we present an experimental study whose aim is to provide empirical evidence on the relevance of UP-resilience. We also study the impact of the order factor and, more specifically, the current orders used in state of the art BnB solvers on the UP-resilience of Max-SAT resolution transformations.

We have implemented a simple procedure to compute the percentage of UPresilience of the transformations. We generate all the possible neighborhoods of the literals and then we check if each literal can be propagated when each of its neighborhoods is satisfied. This naive implementation is time-consuming and increases the solving time of 25% in average. Its purpose is to evaluate the transformation of ISs as well as the learning mechanisms, not to be competitive. The implementation is performed in the solver ahmaxsat [START_REF] Abramé | ahmaxsat: Description and Evaluation of a Branch and Bound Max-SAT Solver[END_REF] 100% and 98%). Furthermore, the solver explores more than three times (resp.

four times) more nodes of the search tree with the IRS learning scheme than with PAT (resp. PAT+). This is clearly due to the fact that SUP detects less ISs with the IRS learning scheme and, thus, provides a worse estimation of LB compared to PAT and PAT+ which leads to less cuts in the search tree. Consequently, ahmaxsat IRS solves much less instances (at least 367 less instances than the other variants) with a higher average solving time for shared instances (at least 138 seconds more than the other variants). From these results, we can conclude that the IRS learning scheme, as it is implemented in ahmaxsat IRS , does not control efficiently the impact of the transformations on the SUP mechanism.

Secondly, the comparison of the PAT and PAT+ learning schemes shows a slight increase of the percentage of learned transformations while keeping a high percentage of UP-resilience (resp. 100% and 98%). Consequently, the average number of decisions as well as the average solving time are slightly reduced.

It is also interesting to observe that the percentage of transformations learned with the PAT+ learning scheme is lower than the one obtained with the UPR learning scheme. This clearly shows that the current patterns do not allow the detection of all UP-resilient transformations. This is also coherent with our theoretical study in Section 5. Finally, the UPR learning scheme outperforms all the other schemes (1407 instances solved in 58.27 seconds on average) when we don't consider the computation time required for checking the UP-resilience of the transformations which provides empirical evidence on the relevance of this property.

Orders and UP-Resilience

In the second set of experiments, we evaluate the impact of the current orders of application of Max-SAT resolution on the UP-resilience of the transformation.

We compare two variants:

• ahmaxsat RP O : applies the Max-SAT resolution steps in reverse propagation order (RPO)

• ahmaxsat SIR : uses the Smallest Intermediary Resolvent (SIR) heuristic described in [START_REF] Abramé | Efficient application of max-sat resolution on inconsistent subsets[END_REF].

The results are presented in Table 2 where UPR* refers to the average percentage of UP-resilience of the Max-SAT resolution transformations of the detected ISs for instances solved by both variants. We observe that the average percentage of UP-resilience is significantly higher with the SIR heuristic (64.8% compared to 57.1% for RPO). Consequently, less decisions are necessary to solve the instances (102,088 compared to 123,028 on average for RPO) and the solving time is reduced (by 27 seconds on average). This shows the importance of the Max-SAT resolution application order factor which has a direct impact on the UP-resilience of the transformations and, thus, on the solver performance. In our theoretical study in Section 5, we also provide an explanation for the seemingly low average percentage of UP-resilience (less than 65% for both orders) by showing that they don't necessarily ensure UP-resilience of certain patterns.

Impact of UP-Resilience

In the last set of experiments, we have implemented a new learning scheme based on the minimum percentage of UP-resilience allowed in the learned transformations of ISs (%UPR IS ) and UCSs (noted %UPR UCS ). We have tested this new learning scheme with %UPR IS and %UPR UCS ranging respectively from 0 to 100 and from 40 to 100. Results are presented in Fig. 13. We observe that the best performance is achieved with %UPR IS and %UPR UCS ranging from 60% to 100%. On these ranges of values, the average percentage of UP-resilience of the learned transformations is always higher than 90%. With values lower than 60%, the average number of decisions increases importantly and so does the average solving time. These results show that UP-resilience quantifies accurately the impact of the transformations on the efficiency of SUP and provide further incentive for our study in Section 5.

Conclusion and Future Work

We have introduced in this paper the notion of UP-resilience which quantifies the impact of Max-SAT resolution transformations on the SUP mechanism. We have shown that, according to the UP-resilience criterion, the main patterns do not have a negative impact on SUP. It contributes to explain theoretically the efficiency of the most used learning scheme which was proved only empirically until now. We also proved that k b -UCSs are UP-resilient with respect to two different orders PRO and PRCO. Then, we generalized this result to k-UCSs where all clauses are binary except one of any size involved in the conflict.

We showed that unlike our orders, the current mechanisms don't necessarily ensure UP-resilience for these patterns. Thus, our orders can help extend the current patterns used in state of the art BnB solvers. Finally, we presented an experimental study providing empirical evidence on the relevance of UPresilience.

To our best knowledge, this is the first work in which UP-resilience is used to characterize the transformations by Max-SAT resolution in order to decide the relevance of their application. Indeed, this can be a starting point of a new approach to extend Max-SAT resolution patterns. In our case, we chose UCS patterns because they present several advantages: the introduction of unit clauses as well as the high frequency of their apparition. We also showed the limits of the current orders of application of Max-SAT resolution. In fact, this is the first work in which the proposed orders are introduced relatively to the structure of the implication graphs representing the possible propagation sequences of an IS.

The prospects of our research include the extension of our studies to k-UCSs in general. It also opens new perspectives for finding orders of application of Max-SAT resolution that ensure UP-resilience or maximize its percentage by thoroughly studying the implication graphs corresponding to the propagation sequences of certain ISs. Another interesting prospect is extending our work on more sophisticated mechanisms that are used to detect disjoint ISs such as Generalized Unit Propagation (GUP) [START_REF] Kuegel | Improved exact solver for the weighted max-sat problem[END_REF] which combines SUP whith Failed Literals (FL) [START_REF] Li | Detecting Disjoint Inconsistent Subformulas for Computing Lower Bounds for Max-SAT[END_REF]. For instance, if the reason of unsatisfiablity of the detected IS after applying GUP can be represented in the form of an implication graph, our results would be applicable to GUP.

Finally, BnB solvers perform poorly on structured instances such as industrial ones. In our opinion, this is mainly due to their inability to consider the structural properties of these instances in the exploration of the search space.

An extended learning mechanism as described in our work may allow to guide the exploration of the search tree by using the learned information as it is done in modern SAT solvers. Thus, the UP-resilience property presented in this paper may be a significant step towards the improvement of BnB Max-SAT solvers performance on industrial instances. Also, increasing knowledge about Max-SAT resolution can be useful for SAT-based solvers, which are mainly efficient on industrial instances, as some solvers, such as EVA [START_REF] Narodytska | Maximum satisfiability using core-guided maxsat resolution[END_REF], already exploit Max-SAT resolution to transform cores returned by SAT solvers.

l

  ∈ I. The empty clause is always falsified. For a unit assignment I = {l}, we denote by Φ| I the formula obtained by reducing Φ by I, i.e, Φ| I = {c ∈ Φ | {l, l} ∩ c = ∅} ∪ {c \ {l} | c ∈ Φ, l ∈ c}. This notation can be extended to any assignment I = {l 1 , l 2 , . . . , l k } as follows: Φ| I = (. . . ((Φ| {l1} )| {l2} ) . . . | {l k } ).

  A simple estimation for LB is the number of the falsified clauses of the formula Φ by the current assignment I. Formally, LB = falsified_clauses(Φ| I ) = |{c ∈ Φ | c| I = }|. As this simple estimation is often quite far from the best accessible solution, BnB Max-SAT solvers refine it by calculating the number of disjoint

  and c ∈ ψ is reduced by l and propagates l } {( c , l, c) | l ∈ I and c = {l} ∈ ψ} {(l, , c) | l ∈ I and c ∈ ψ is falsified by I and l ∈ ψ} The directed edges are labeled by clauses and the nodes are omitted in G.

  most used method to treat ISs, outlined in Algorithm 1, is based on the Max-SAT resolution inference rule defined below. A Max-SAT resolution transformation requires an implication graph describing the sequence of propagations leading to the detection of the IS. The transformation is usually done in the reverse order of propagation. The treatment performed by Max-SAT resolution(Φ, c 1 , c 2 , var(l)) (line 6 in Algorithm 1) consists in deleting the clauses c 1 and c 2 and adding the compensation clauses and the resolvent clause cr (also returned after the transformation) to the formula as described in the Max-SAT resolution rule defined as follows:.

Algorithm 1 :Output: the transformed formula 1 begin 2 c 1 ← 3 while c 1 = do 4 l 5 c 2 ← 7 c 1 1 .

 1213452711 Max-SAT resolution Transformation of an IS Input: a CNF formula Φ, an implication graph G of an IS of Φ src G ( ); ← the last propagated literal in G; src G (l); 6 cr ← max_resolution(Φ, c 1 , c 2 , var(l)); We consider the IS ψ = {{x 1 }, {x 2 }, {x 3 }, {x 3 , x 4 }, {x 1 , x 2 , x 4 }} detected by the sequence of unit propagations represented in the form of an implication graph on the left in Figure 1. The Max-SAT resolution transformation of ψ with respect to the variable sequence S = x 4 , x 3 , x 2 , x 1 (in the reverse order of propagation) is given on the right in Figure 1.

Figure 1 :

 1 Figure 1: Implication graph corresponding to a propagation sequence of ψ and its transformation by Max-SAT resolution, where compensation clauses for each step are represented in boxes

Definition 4 (Example 2 .

 42 Unit Clause Subset). Let Φ be a CNF formula and k a natural number. A k-Unit Clause Subset where k ≥ 2, denoted k-UCS, is a set of clauses {c 1 , ..., c k } ⊆ Φ such that there exists a sequence of Max-SAT resolution steps on c 1 , ..., c k that produces a unit clause reslovent. In particular, if ∀i ∈ {1, ..., k} we have |c i | = 2, it is a binary k-UCS, denoted k b -UCS. The patterns (P 1) and (P 2) which are learned in state of the art BnB solvers, correspond respectively to a 2 b -UCS and a 3 b -UCS.

Figure 2 :

 2 Figure 2: Implication graph corresponding to a propagation sequence of ψ and its transformation by Max-SAT resolution, where compensation clauses for each step are represented in boxes

Example 4 .

 4 of detected ISs and the increase of the number of decisions. More specifically, Max-SAT resolution transformations may result in a "fragmentation" of the information contained in the original clauses of the formula. This phenomenon, showcased in Example 4, occurs when clauses are fragmented into two (or more) clauses after transformation by Max-SAT resolution which may obstruct their exploitation by the SUP mechanism. In this case, the original information can only be retrieved by applying Max-SAT resolution between the fragmented clauses. We consider the IS ψ = {{x 1 }, {x 2 }, {x 3 }, {x 3 , x 4 }, {x 1 , x 2 , x 4 }}, introduced in Example 1, detected by the implication graph G in Figure 1 and whose Max-SAT resolution transformation with respect to the reverse order of propagation, corresponding to the sequence S = x 4 , x 3 , x 2 , x 1 , is represented on the right in the same figure. If the unique neighbor of x 1 in the implication graph is set to true in the transformed IS, we obtain Θ(ψ, S)

Example 5 .Example 6 .

 56 We consider the IS ψ = {{x 1 }, {x 2 }, {x 3 }, {x 3 , x 4 }, {x 1 , x 2 , x 4 }}, introduced in Example 1, detected by the implication graph G in Figure1. We showed in Example 4 that the fragmentation phenomenon occurs since the literal x 1 can't be propagated in Θ(ψ, S)| neigh(x1) . Thus, the described transformation is not UP-resilient in the implication graph G.The previous definition of UP-resilience depends on the neighborhoods of the literals in the implication graph. However, the same IS can be detected by several sequences of propagation steps which can be described by distinct implication graphs. We consider the ISψ = {{x 1 }, {x 2 }, {x 3 }, {x 3 , x 4 }, {x 1 , x 2 , x 4 }},introduced in Example 1. In addition to the implication graph presented in the original example represented on the left in Figure 3, another sequence of propagations, corresponding to the implication graph represented on the right in the same figure, can lead to the detection of the IS ψ. The propagation sequences corresponding to the same implication graph are considered as equivalent.

Figure 3 :

 3 Figure 3: Implication graphs corresponding to the possible propagation sequences of ψ

  Moreover, since |L | = n, we know by induction that ∀N ∈ pneigh(L ) : ∈ N or every literal l in L can be propagated in Θ(ψ, S)| N \{l } . In particular, ∈ N 1 or every literal l in L can be propagated in Θ(ψ, S)| N1\{l } . Also, The transformation Θ(ψ, S) is UP-resilient for L and particularly for l and thus, we have ∀N ∈ pneigh(l) : ∈ N or l can be propagated in Θ(ψ, S)| N . In particular, ∈ N 2 or l can be propagated in Θ(ψ, S)| N2 .

  every literal l in L and l can be propagated respectively in Θ(ψ, S)| N1\{l } and Θ(ψ, S)| N2 . Therefore, the clauses that ensure the propagation of every literal l in L in Θ(ψ, S)| N1\{l } also ensure their propagation in Θ(ψ, S)| (N1∪N2)\{l } and, similarly, the clauses that ensure the propagation of l in Θ(ψ, S)| N2 also ensure its propagation in Θ(ψ, S)| (N1∪N2)\{l} .

Figure 4 :

 4 Figure 4: Implication graphs corresponding to the possible propagation sequences for an IS containing the premises of pattern (P 1 )

Figure 5 :

 5 Figure 5: Implication graphs corresponding to the possible propagation sequences for an IS containing the premises of pattern (P 2 )

Figure 6 :

 6 Figure 6: Implication graphs corresponding to the possible propagation sequences for an IS matching the premise of pattern (P 3)

  x 4 }, }. The empty clause appears in the possible neighborhoods of the literals x 4 and x 4 . The propagation of the literal x 3 with respect to its possible neighborhood {x 4 }, not containing the empty clause, is ensured by the clause {x 3 , x 4 }. Furthermore, the propagation of literals x 1 and x 2 with respect to their possible neighborhood {x 4 }, not containing the empty clause, is ensured by the clauses {x 1 , x 4 } and {x 1 , x 2 , x 4 }.

Figure 7 :

 7 Figure 7: Implication graph corresponding to the Max-SAT resolution transformation of ψ with respect to SIR

Lemma 1 .

 1 studied k-UCSs. More specifically, we study the portion of the graph representing the propagation sequence of the detected k-UCS which is delimited by the FIUP and the empty clause. This characterization is established by the following lemma: Let k ≥ 2 and ψ be a k-UCS whose clauses are binary except for the conflict clause of size s ≥ 2, recognized by the FUIP l in an implication graph G of an IS such that |succ(l)| = s. Then, there exists exactly s disjoint paths from l to in G.

Proposition 4 .

 4 Let k ≥ 2 and ψ be a k b -UCS recognized by the FUIP l in an implication graph G of an IS. Then, |succ(l)| = 2.

Figure 8 :

 8 Figure 8: Implication graphs corresponding to the possible propagation sequences for k b -UCSs.

Figure 9 :

 9 Figure 9: Implication graphs corresponding to the possible propagation sequences of ψ in Example 9 and the application of Max-SAT resolution steps relatively to RPO

Theorem 3 .

 3 Let k ≥ 2 and ψ be a k-UCS whose clauses are binary except for the conflict clause c of size |c| = s ≥ 3, recognized by the FUIP l in the implication graph G of an IS such that |succ(l)| = s. The transformation of ψ with respect to MPRO is UP-resilient.

Figure 10 :

 10 Figure 10: Implication graphs corresponding to the possible propagation sequences for k-UCSs with binary clauses except for the conflict clause

Figure 11 :Corollary 3 .

 113 Figure 11: Application of Max-SAT resolution steps on the variables of the non binary clause c by induction on its size

Example 10 . 1 , l 2 , l 3 and l 4 .Figure 12 .

 1012412 Figure 12. Clearly, the literal l 4 can't be propagated in Θ(ψ, S)| neigh(l4) =

Figure 12 :

 12 Figure 12: Implication graphs corresponding to the possible propagation sequences of ψ in Example 10 and the application of Max-SAT resolution steps relatively to RPO

Figure 13 :

 13 Figure 13: Impact of the minimum percentage of UP-resilience allowed for learning the transformations of ISs and UCSs

Table 1 :

 1 Impact of learning schemes on the efficiency of BnB Max-Sat solvers

Table 2 :

 2 Impact of current Max-SAT resolution application orders on the UP-resilience of transformations

This paper is based on work published in [1] and [2]. This work has been partially funded by the French National Research Agency, reference ANR-16-C40-0028.

We prove that the Max-SAT resolution transformation relatively to the order O = M P RO(p 1 , ..., p s ) is UP-resilient:

• The same arguments in the proof of Theorem 1 ensure the UP-resilience of the transformation respectively to O for l pi j where 1 ≤ i ≤ s and 1 ≤ j < n i as well as l and all the literals involved in its propagation. Furthermore, all the neighborhoods of literals l 1 , ..., l s contain the empty clause.

. Clearly, the clause c = {l, l pi ni-1 , l pi ni } obtained by the application of Max-SAT resolution on var(l pi ni-1 ) ensures the propagation of l pi ni in any of these neighborhoods when l pi ni-1 is set to true since l is propagated by the unit resolvent clause {l}. We deduce that the transformation relatively to the order O is UP-resilient for l pi ni where 1 ≤ i ≤ s and n i > 1.

• We still need to prove the UP-resilience of the transformation for literals l pi ni = l i when n i = 1, with respect to their possible neighborhoods {l, l j } for j ∈ {1, .., s} \ {i} not containing the empty clause. For this end, we prove by induction on |c| ≥ 3 that the compensation clauses produced by the Max-SAT resolution steps on var(l 1 ), ..., var(l s ) ensure the propagation of each literal l i if we consider the neighborhoods as mentioned above.

For simplification, in the first Max-SAT resolution step, we replace c by the clause c = {l, l 1 , ..., l s }. This doesn't affect our result since we only omit a single clause containing the literal l: (denoted pms) and weighted partial Max-SAT (denoted wpms). BnB Max-SAT solvers are not competitive on industrial instances, which is why they were omitted. We have made 143856 separate runs of the solver which, in our opinion, is sufficient to show the impact of the studied components on the solver behavior.

All the experiments are performed on machines equipped with Intel Xeon 2.4

Ghz processors and 24 Gb of RAM and running under a GNU/Linux operating system. The cutoff time is fixed to 1800 seconds per instance.

Learning Schemes and UP-Resilience

In the first set of experiments, we evaluate the impact of different learning schemes on the behavior of BnB Max-SAT solvers. We consider the following variants:

• ahmaxsat IRS : uses the learning scheme of MiniMAXSAT [START_REF] Heras | MiniMaxSAT: An efficient weighted maxsat solver[END_REF]. A transformation is learned if all the intermediary resolvents contain less than four literals.

• ahmaxsat P AT : learns the transformations when the ISs match the three main patterns presented in Section 2.2.4.

• ahmaxsat P AT + : learns the transformations when the ISs match the main patterns or the extended set of patterns including UCSs, presented in Section 2.2.4.

• ahmaxsat U P R : learns only UP-resilient transformations of ISs.

Table 1 shows the obtained results. For each variant, the columns S(T ), D and L represent respectively the number of solved instances with the average solving time, the average number of decisions and the percentage of learned 1 https://maxsat-evaluations.github.io/2019/history.html


ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

  Laboratoire Cellules Circulantes Rares Humaines, CHU de Montpellier, Université de Montpellier, 34000 Montpellier, France. c-panabieres@chu-montpellier.fr Les Cellules Tumorales Circulantes (CTC) sont des cellules cancéreuses qui proviennent de la ou des tumeurs primaires et / ou métastatiques. Elles peuvent être détectées dans des échantillons de sang périphérique avec différentes technologies mais leur identification et leur caractérisation nécessitent des méthodes d'analyse extrêmement sensibles et spécifiques. Catherine Alix-Panabières dirige depuis 2013 le Laboratoire Cellules Circulantes Rares Humaines (LCCRH), un laboratoire leader dans le domaine des Cellules Tumorales Circulantes (CTCs). Elle travaille sur cette thématique depuis une vingtaine d'année et a inventé le terme « Biopsie Liquide » en 2010 avec le Pr Klaus Pantel (Hambourg, Allemagne). Ses travaux ont notamment été récompensés par le prix « Gallet et Breton » de l'Académie Nationale de Médecine en 2012 et par un Award lors de « l'American Association for Cancer Research Annual Meeting » à Washington en 2017 pour la publication d'un article sur la culture des CTCs in vitro. Publications récentes : Boyer M, Cayrefourcq L, Garima F, Foulongne V, Dereure O, Alix-Panabières C. Liquid Biopsy in Merkel Cell Carcinoma: Detection of Circulating Tumor Cells and Identification of the Polyomavirus Status in Single Tumor Cells. Sci Rep. In Press. Cayrefourcq L, De Roeck A, Garcia C, Stoebner PE, Fichel F, Garima F, Perriard F, Daures JP, Meunier L, Alix-Panabières C.S100-EPISPOT: A New Tool to Detect Viable Circulating Melanoma Cells. Cells. 2019 Jul 20;8(7). Pantel K, Alix-Panabières C. Liquid biopsy and minimal residual disease -latest advances and implications for cure. Nat Rev Clin Oncol. 2019 Jul;16(7):409-424. Soler A, Cayrefourcq L, Mazard T, Babayan A, Lamy PJ, Assou S, Assenat E, Pantel K, Alix-Panabières C. Autologous cell lines from circulating colon cancer cells captured from sequential liquid biopsies as model to study therapy-driven tumor changes. Sci Rep. 2018 Oct 29;8(1):15931. Mazel M, Jacot W, Pantel K, Bartkowiak K, Topart D, Cayrefourcq L, Rossille D, Maudelonde T, Fest T, Alix-Panabières C. Frequent expression of PD-L1 on circulating breast cancer cells. Mol Oncol. 2015 Nov;9(9):1773-82. Vendredi 13 Novembre, 11h15 " Biopsie liquide : focus sur le mélanome et le carcinome de Merkel "