On the Resiliency of Unit Propagation to Max-Resolution

1 Introduction

The Max-SAT problem consists in finding, for a given CNF formula, a Boolean assignment of the variables of this problem which maximizes the number of satisfied clauses.

Among the methods to solve the Max-SAT problem, Branch and Bound (BnB) algorithms (e.g. AKMAXSAT [K¨ugel, 2010], AHMAXSAT [Abram´e and Habet, 2014a; 2014b], WMAXSATZ [Li et al., 2010; 2007]) have shown their efficiency, especially on random and crafted instances. They explore the whole search space and compare, at each node of the search tree, the current number of falsified clauses plus an (under-)estimation of the ones which will become falsified (the lower bound, LB) to the best solution found so far (the upper bound, UB). If LB ≥ UB, then no better solution can be found in the current branch and a backtrack is performed. The estimation of the remaining inconsistencies is a key component of BnB solvers: on the one hand, it is one of the most time-consuming components and on the other hand the quality of the LB leads the backtracks and determines the number of explored nodes.

Efficient BnB Max-SAT solvers compute the lower bound by counting the disjoint inconsistent subsets (IS) of the formula. They use unit propagation based methods [Li et al., 2005; 2006] to detect the inconsistent subsets. Each detected IS must be treated to ensure it will be counted only once. One of the existing treatments is based on the max-resolution rule [Larrosa and Heras, 2005; Heras and Larrosa, 2006; Bonet et al., 2007]. It consists in applying several maxresolution steps on the clauses of the IS. The resulting formulas are equivalent to the original ones, thus the transformations can be learned to make the lower bound computation more incremental. However, it has been observed empirically that learning the max-resolution transformations may affect negatively the quality of the lower bound estimation. For this reason, existing solvers learn transformations selectively according to various criteria.

We study in this paper the impact of the max-resolution transformations on the UP mechanism. We show that in some cases the information which can be used by UP in the original formula are, after transformations, fragmented in several clauses. In such situation, UP may be less efficient in the transformed formula than in the original one. We introduce the notion of UP-resiliency to characterize the transformations which are not affected by fragmentation and more generally to measure the impact of the transformations on the UP mechanism. We show that according to this criterion, the most used learning scheme does not affect UP. It contributes to explain from a theoretical point of view the empirical results obtained in the last ten years on the development of inference rules [Li et al., 2007]. The results of the experimental study we have performed confirm the relevance of the UPresiliency criterion. They give insight on the behavior of the learning mechanism and open new perspectives of development.

This paper is organized as follows. In Section 2, we give the basic definitions and notations used in this paper. We present in Section 3 the IS learning mechanism and we motivate our contribution. We introduce UP-resiliency in Section 4 and present an experimental study on it in Section 5 before concluding in Section 6.

2 Definitions and Notations

A formula Φ in conjunctive normal form (CNF) defined on a set of propositional variables X = {x1, . . . , xn} is a conjunction of clauses. A clause cj is a disjunction of literals and a literal l is a variable xi or its negation xi. Alternatively, a formula can be represented as a multiset of clauses Φ = {c1, . . . , cm} and a clause as a set of literals cj = {lj1 , . . . , ljk }. An assignment can be represented as a set I of literals which cannot contain both a literal and its negation. If xi is assigned to true (resp. false) then xi ∈ I (resp. xi ∈ I). I is a complete assignment if |I| = n and it is partial otherwise. A literal l is said to be satisfied by an assignment I if l ∈ I and falsified if l ∈ I. A clause is satisfied by I if at least one of its literals is satisfied, and it is falsified if all its literals are falsified. By convention, an empty clause (denoted by □) is always falsified. A subset ψ of Φ is inconsistent if there is no assignment which satisfies all its clauses. For a unit assignment I = {l}, we denote by Φ|I the formula obtained by applying I on Φ. Formally: Φ|I = {cj | cj ∈ Φ, {l, l} ∩ cj = ∅} ∪ {cj \ {l} | cj ∈ Φ, l ∈ cj}. This notation can be extended to any assignment I = {l1, l2, . . . , lk} as follows: Φ|I = (. . . ((Φ|{l1})|{l2}) . . . |{lk}). Eventually, solving the Max-SAT problem consists in finding a complete assignment which maximizes (minimizes) the number of satisfied (falsified) clauses of Φ. There exists other variants of Max-SAT (weighted, partial and weighted partial Max-SAT) which are not considered in this paper. Nevertheless, the presented results can be extended to these variants.

3 Preliminaries andMotivations

We present in this section the mechanisms of IS detection and transformation as well as the learning schemes used in recent solvers. Then, we show through an example that IS transformations can impact UP efficiency.

3.1 IS Detection

Unit propagation (UP) consists in iteratively satisfying the literals which appear in unit clauses until a conflict is found (an empty clause) or no more unit clause remains. When a conflict is detected, the clauses which have led to it by propagation form an inconsistent subset of the formula.

The propagation steps can be represented by an implication graph G = (V,A) which is a directed acyclic graph where the nodes V are the propagated literals and each arrow of A is tagged with the clause causing the propagation [MarquesSilva and Sakallah, 1999]. The special node □ is used to represent the empty clause.

In the remaining of this paper, we will use the following additional notations. Let us consider a sequence of propagation steps described by the implication graph G = (V,A). For each literal li ∈ V , we denote predG(li) the predecessors of li in G and succG(li) its successors. We can define the neighborhood of li in G as neighG(li) = predG(li) ∪ succG(li). Note that this last definition can be extended to any subset V ′ of V as follows neighG(V ′ ) = ⋃li∈V ′ neighG(li) \ V ′ .

3.2 IS Transformation

Once detected, IS must be transformed to ensure that they will be counted only once. The most used transformation method is based on the max-resolution inference rule [Larrosa and Heras, 2005; Heras and Larrosa, 2006; Bonet et al., 2007].

Definition 1 (Transformation by max-resolution). Let Φ be a formula and ψ an IS of Φ. For all variable xi s.t. ∃!cj = {xi, lj1 , . . . , ljs } ∈ ψ, xi ∈ cj and ∃!ck = {xi, lk1 , . . . , lkt } ∈ ψ, xi ∈ ck, we denote by θ(ψ, xi) the set of clauses obtained from ψ after application of the maxresolution rule between cj and ck on xi. Formally:

with cr = {lj1 , . . . , ljs , lk1 , . . . , lkt } the resolvent and cc1 = {xi, lj1 , . . . , ljs , lk1 , lk2 , . . . , lkt }, cc2 = {xi, lj1 , . . . , ljs , lk2 , lk3 , . . . , lkt }, . . . , cct = {xi, lj1 , . . . , ljs , lkt }, cct+1 = {xi, lk1 , . . . , lkt , lj1 , lj2 , . . . , ljs }, cct+2 = {xi, lk1 , . . . , lkt , lj2 , lj3 , . . . , ljs }, . . . , cct+s = {xi, lk1 , . . . , lkt , ljs } the compensation clauses. For any sequence S = (xi1 , . . . , xik ) of variables appearing in ψ, we denote by Θ(ψ, S) the set of clauses obtained from ψ after application of the maxresolution rules on xi1 then xi2 and so forth. Formally Θ(ψ, S) = θ(. . . θ(θ(ψ, xi1 ), xi2 ) . . . , xik ).

The following example illustrates the transformation of an IS by max-resolution.

Example 1. Let us consider a formula Φ1 = {c1, . . . , c6} with c1 = {x1}, c2 = {x2}, c3 = {x1, x2, x3}, c4 = {x3, x4}, c5 = {x3, x5} and c6 = {x4, x5}. The application of UP leads to the propagation sequence (x1@c1, x2@c2, x3@c3, x4@c4, x5@c5) (meaning that x1 is propagated by c1, then x2 by c2, etc.). The clause c6 is empty and the corresponding implication graph is shown on Fig. 1a. Hence, Φ1 is an inconsistent subset. Its transformation by max-resolution is done as follows. Max-resolution is first applied between c6 and c5 on the variable x5. The intermediary resolvent cr1 = {x3, x4} is produced as well as the compensation clauses cc1 = {x3, x4, x5} and cc2 = {x3, x4, x5}. The original clauses c5 and c6 are removed from the formula.

(a) Implication graph Then, max-resolution is applied between the intermediary resolvent cr1 and the next original clause c4 on the variable x4 and so forth. Fig. 1b shows the max-resolution steps with in boxes the compensation clauses. After complete transformation, we obtain the formula Φ′1 = {□, cc1, cc2, cc3, cc4, cc5} with cc3 = {x1, x2, x3}, cc4 = {x2, x3} and cc5 = {x1, x2}.

Figure 1: Implication graph and Max-SAT resolution steps applied on the formula Φ1 from Example 1.

3.3 Existing Learning Schemes

Recent BnB solvers apply learning in the sub-part of the search tree under some conditions. Two main learning schemes are used. The first one learns a transformation only if all the intermediary resolvents are smaller than four [Heras et al., 2008]. The second scheme learns transformations of the IS part matching the main following patterns [Li et al., 2007]:

These patterns have been recently extended in [Abram´e and Habet, 2014c]. Note that solvers do not learn only the transformations of whole IS. They can also learn the transformation of unit clause subsets (UCS) which are subsets of the formula which do not include unit clauses and which produce, after transformation by max-resolution, unit resolvent clauses.

3.4 Fragmentation Phenomenon

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 UP. However, experimental analysis [Abram´e and Habet, 2014c] shows that increasing learning slightly may deteriorate significantly the solver performance. The reasons cited above cannot explain this behavior.

Abram´e and Habet [2014c] have also shown that the maxresolution transformations may result in a "fragmentation" of the information contained in the original clauses of the formula. Clauses which can have been used in UP are, after transformation by max-resolution, fragmented in two (or more) clauses. The original information can only be retrieved by applying max-resolution between them.

Example 2. Let us consider the formula Φ2 = {c1, c2, c3, c4, c5, c6, c7} with c6 = {x4, x6} and c7 = {x5, x6} (c1, . . . , c5 are the same as in Example 1). The application of UP leads to the propagation sequence (x1@c1, x2@c2, x3@c3, x4@c4, x5@c5, x6@c6) and the clause c7 is empty. The corresponding implication graph is shown in Fig. 2. If we apply max-resolution according to the sequence (x4, x6, x5, x3, x2, x1), we obtain the formula Φ′2 = {□, cc3, cc4, cc5, cc6, cc7, cc8, cc9} with cc6 = {x3, x4, x6}, cc7 = {x3, x4, x6}, cc8 = {x3, x5, x6} and cc9 = {x3, x5, x6} (cc3, cc4 and cc5 are the same as in Example 1).

Let us assign x4 and x5 to true. In the original formula Φ2, the subset {c6, c7} is inconsistent and the application of UP leads to the following propagation sequence (x1@c1, x2@c2, x3@c3). In the transformed formula Φ′2 , the clauses cc7 and cc9 are reduced and become respectively {x3, x6} and {x3, x6} but no propagation steps can be performed. Note that if we apply max-resolution between this two clauses on x6 we obtain the unit resolvent {x3} but the sole UP cannot exploit these two clauses. Thus we can say that the information which may have led to the propagation of x3 is fragmented.

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

4 UP-Resiliency

We study in this section the resiliency of UP to transformations. We introduce the notion of UP-resiliency of a transformation to characterize the transformations which have no negative impact on UP and to quantify this impact. We discuss the UP behavior on the formula resulting from UPresilient transformations and we show that the most used learning scheme does not affect UP.

4.1 In an Implication Graph

When fragmentation occurs, the compensation clauses which may propagate a literal li of the original implication graph G contain additional literals which are not in the original neighborhood of li in G. Thus, to detect if a transformation is not affected by the fragmentation phenomenon, we can rely on the capability of UP to propagate the literals of the original implication graph G when only their neighborhood literals in G are set to true. We said that such transformations are UPresilient.

Definition 2 (UP-resiliency in an implication graph). Let Φ be a formula, ψ an IS detected by the propagation steps described by the implication graph G = (V,A) and S a sequence of variables appearing in ψ. For a literal li ∈ V , we say that the transformation Θ(ψ, S) is UP-resilient for li in G iff □ ∈ neighG(li) or li can be propagated in Θ(ψ, S)|neighG(li).

We say that Θ(ψ, S) is UP-resilient in G for a subset V ′ of V iff it is UP-resilient ∀li ∈ V ′ and that it is UP-resilient in G iff it is UP-resilient for V .

Note that the neighborhoods which include the special node □ are not valid assignments. All transformations are considered UP-resilient for literals with such neighborhood.

4.2 Generalization

The definition of the UP-resiliency given in the previous section depends on the neighborhood 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.

Example 3. Let us consider the formula Φ1 from Example 1. In addition to the one presented in the original example, two other sequences of propagation steps can lead to the detection of the inconsistent subset while changing the value given to the propagated variables: (x1@c1, x2@c2, x3@c3, x4@c4, x5@c6) and (x1@c1, x2@c2, x3@c3, x5@c5, x4@c6). Note that we ignore the propagation sequences varying only by the order of the propagation steps.

With the previous definition, the UP-resiliency of a transformation may vary depending on how the IS have been detected. To overcome this limitation, we propose to consider all the possible ways (i.e. sequences of propagation steps) to detect the IS. Let us first define the set of the possible neighborhoods of a literal appearing in an inconsistent subset.

Definition 3 (Possible neighborhoods). Let Φ be a formula and ψ an IS. For a literal li appearing in ψ clauses, we can define its possible neighborhoods as pneighψ(li) = {neighG(li), ∀ implication graph G = (V,A) of ψ s.t. li ∈ V }. This definition can be naturally extended to any set of literals.

Then we can give a general definition of the UP-resiliency which does not depend anymore of the propagation steps which have led to the IS discovery.

Definition 4 (UP-resiliency). Let Φ be a formula, ψ an IS and S a sequence of variables appearing in ψ. For a literal li appearing in ψ, we say that the transformation Θ(ψ, S) is UP-resilient for li iff for all nk ∈ pneighψ(li): □ ∈ nk or li can be propagated in Θ(ψ, S)|nk .

We say that Θ(ψ, S) is UP-resilient for a set of literals L appearing in ψ iff it is UP-resilient ∀li ∈ L and that it is UPresilient iff it is UP-resilient for all the literals appearing in ψ.

Similarly, we can quantify a transformation impact on UP by defining its percentage of UP-resiliency as the percentage of couples (li, nk) s.t. □ ∈ nk or li can be propagated in Θ(ψ, S)|nk .

4.3 Impact on the IS Detection

One of the most interesting properties of the UP-resilient transformations is the capability to retrieve the propagations which are not necessary anymore to an inconsistent subset. We have seen that if a transformations is UP-resilient for a literal li, then li can be propagated in the transformed formula when the literals of one of its possible neighborhoods is set to true. We now show that this property can be extended to sets of literals, i.e. that if a transformation is UP-resilient for a set of literals L, then the literals of L can be propagated in the transformed formula if the literals of one of L possible neighborhoods are set to true.

Property 1. Let Φ be a formula, ψ an IS, S a sequence of variables appearing in ψ and L a set of literals appearing in ψ. If the transformation Θ(ψ, S) is UP-resilient for L then for all nk ∈ pneighψ(L): □ ∈ nk or all L literals can be propagated in Θ(ψ, S)|nk .

Proof. Let ψ be an IS detected thanks to the propagation steps described by a implication graph G and S = (xi1 , . . . , xim ) a sequence of ψ variables. We assume that the partial transformation Θ(ψ, (xi1 , . . . , xih )) (with h < m) has already be applied. We denote by G|(xi1 ,...,xih ) the updated implication graph obtained by replacing the resolved clauses by the intermediary resolvent produced. For every literal lij s.t. lij , lij /∈ {xi1 , . . . , xih } the compensation clauses providing UP-resiliency for lij in G can only be obtained by (we assume that such clause has not yet been obtained and that □ /∈ neighG(lij )): (1) applying max-resolution on lij if □ /∈ succG|(xi1 ,...,xih ) (lij ) or (2) applying max-resolution on a successor lik of lij if □ ∈ succG(lik ). These two points can be easily proved by observing the compensation clauses obtained when we transform clauses containing lij or lij . In any other cases, the compensation clauses produced do not contain lij or include literals which are not in lij neighborhood in G. Also note that we present here only the information which is relevant to our demonstration. These conditions are necessary but not sufficient to obtain li UP-resiliency.

We can now prove the property. Let us proceed by induction on the size of a set of literals L appearing in ψ. Base: If |L| = 1 then obviously the property is verified. Inductive step: We assume that the property holds for every L′ s.t. |L′ | < n and we now consider a set of literals L s.t. |L| = n and an implication graph G = (V, A) of ψ s.t. L ∈

V . Let us consider the last literal lij of L in S.

If the UP-resiliency in G for lij has been obtained by applying max-resolution on lij (case 1), then the compensation clauses providing UP-resiliency for lij cannot contain literals from L \ {lij }. Thus neighG(L) is sufficient to propagate lij in the transformed formula. By assumption we know that neighG(L\{lij }) propagate L\{lij } in the transformed formula thus the property holds for L.

Otherwise, lij UP-resiliency have been obtained thanks to case (2). We consider the first literal lik of L which have obtained UP-resiliency by applying max-resolution on one of its successors lio (case (2)). We can distinguish to cases:

• if neighG|(xi1 ,...,xio-1 ) (lik ) ∩ L = ∅, then neighG(L) is sufficient to propagate lik in the transformed formula. As previously, by assumption we know that neighG(L\ {lik }) propagates L \ {lik } in the transformed formula thus the property holds for L.
• otherwise, ∀lip ∈ neighG|(xi1 ,...,xio-1 ) (lik ) ∩ L, we know that the clauses providing UP-resiliency for lip have not yet be obtained. After application of maxresolution on lio , we obtain the transformed implication graph G|(xi1 ,...,xio ) and □ ∈ neighG|(xi1 ,...,xio ) (lip ). If □ ∈ neighG(lip ) then □ ∈ neighG(L) and the property holds. Otherwise, the transformation cannot be UPresilient in G for lip and it contradicts the initial assumption.

The same reasoning can be made for every implication graph G of ψ, thus the property holds for any set of literals of size n.

When a subset ψ′ of an IS ψ is not necessary anymore (for instance when ψ is not minimal), this property ensure that UP can perform the same propagations in the transformed formula than in the original clauses of ψ′ .

Example 4. Let us consider again the formula Φ1 from Example 1 and its UP-resilient transformation in Φ′1 . If we assign x4 and x5 to true, the clause c6 is falsified while c4 and c5 are satisfied. The application of UP leads to the following propagation steps: (x1@c1, x2@c2, x3@c3). If we apply UP on the transformed formula Φ′1 , we obtain the propagation steps: (x3@cc2, x2@cc4, x1@cc3). Note that the same propagations are performed in the transformed formula as in the original one. The same propagations can be done in the formula Φ2 with the same assignments. But if we consider the formula Φ′2 obtained by the non UP-resilient transformation presented in Example 2, no propagation can be performed.

4.4 UP-Resiliency of the Existing Patterns

Empirical results [Li et al., 2007] have shown that the existing learning schemes are efficient, but until now there was no theoretical results to explain it. The following property shows that there exist transformations which are UP-resilient for the existing patterns presented in Section 3.3.

Property 2. Let Φ be a formula and ψ an IS. For any ψ′ ⊂ ψ such that ψ′ matches one of the pattern P1, P2 or P3 there exists a sequence S of ψ variables s.t. Θ(ψ, S) is UP-resilient for ψ′ .

Proof. (sketch) For each li ∈ ψ′ and each nk ∈ pneighψ(li), it is simple to check that □ ∈ nk or li can be propagated in Θ(ψ, S)|nk .

5 Experimental Study

We have implemented a simple procedure to compute the percentage of UP-resiliency of the transformations. We generate all the neighborhoods of the literals and then we check if each literal can be propagated when each one 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 IS transformation and learning mechanisms, not to be competitive. The implementation is performed in the solver AHMAXSAT, which was ranked first in three out of nine categories during the last Max-SAT Evaluation 1 .

We have run all the variants presented below on the unweighted and weighted random and crafted instances of the Max-SAT Evaluation 2013. We did not include partial and industrial instances. We have made 66,501 separate runs of the solver. In our opinion, it is sufficient to show the impact of the studied components on the solver behavior. Nevertheless, the presented results can be extended to these instance categories. 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.

1 http://maxsat.ia.udl.cat:81/13

5.1 Impact of the Max-Resolution Application Order on the UP-resiliency

We first evaluate the impact of the order of application of the max-resolution steps on the UP-resiliency of the transformation. We compare two variants:

• AHMAXSAT-RPO applies the max-resolution steps in reverse propagation order
• AHMAXSAT-SIR uses the smallest resolvent heuristic described in [Abram´e and Habet, 2014a].

The results are presented in Table 1. We can observe that the average percentage of UP-resiliency of the transformations is significantly higher with the SIR heuristic (54% vs. 60%). Consequently, less decisions are necessary to solve the instances (123,028 vs. 102,088 in average) and the solving time is reduced (135.5 vs. 108.4 seconds in average). It shows that max-resolution application order has an important impact on the UP-resiliency of the transformations, and thus on the solver performance.

5.2 Impact of the Existing Learning Schemes on the UP-resiliency

In the second set of experiments, we evaluate the impact of the existing learning schemes on the learned transformation UP-resiliency. We consider the following variants:

• AHMAXSAT-IRS uses the learning scheme of MINIMAXSAT [Heras et al., 2008]. A transformation is learned if all the intermediary resolvents contain less than four literals.
• AHMAXSAT-PAT learns the transformations when IS match the patterns presented in Section 3.3.
• AHMAXSAT-PAT+ learns the transformations when IS match the patterns presented in Section 3.3 or the extended sets of patterns presented in [Abram´e and Habet, 2014c].
• AHMAXSAT-UPR learns the transformations of the IS and UCS which are UP-resilient.

Table 2 shows the results obtained. We can first observe that the IRS learning scheme behaves very differently than the PAT and PAT+ ones. It learns in average 80% of the transformations (columns %L) while PAT and PAT+ learn less than 20% of them. The average percentage of UP-resiliency of the transformations learned by the IRS learning scheme (columns %UPRL) is relatively low (78%) compared to the ones of PAT

and PAT+ (respectively 100% and 96%). Consequently, UP detects IS less efficiently with the IRS learning scheme than with the PAT and PAT+ ones. Thus, the solver explores four times more nodes of the search tree (columns D) than with PAT or PAT+ and it solves less instances with a higher average solving time (columns S(T)). 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 UP mechanism.

The comparison of the PAT and PAT+ learning schemes shows a slight increase of percentage of transformations learned for the latter (columns %L) while keeping a high percentage of UP-resiliency (96%). 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 similar to the one obtained with the UPR learning scheme. The detailed results show that on the crafted instances, the PAT+ learning scheme does not detect all the UP-resilient transformations. From this observation, we can conclude that the PAT+ learning scheme can be improved.

5.3 UP-resiliency Based Learning Schemes

We have implemented a new learning scheme based on the minimum percentage of UP-resiliency allowed in the learned transformations of IS (noted %UPRIS) and UCS (noted %UPRUCS). We have tested this new learning scheme with %UPRIS and %UPRUCS ranging respectively from 0 to 100 and from 40 to 100. Results are presented in Fig. 3.

We can observe that the best results are obtained with %UPRIS and %UPRUCS ranging from 60% to 100%. On these ranges of values, the average UP-resiliency percentage of the learned transformation is always higher than 90%. With values lower than 60%, the average number of decisions increases importantly and so does the average solving time. It shows that UP-resiliency quantifies accurately the transformation impact on UP efficiency.

6 Conclusions

We have introduced in this paper the notion of UP-resiliency of a transformation which quantifies the impact of the maxresolution rule on UP. We have shown that, according to UPresiliency criterion, the most used learning scheme based on patterns does not affect UP. It contributes to explain theoretically the learning scheme efficiency which was proved only empirically until now. The results of the experimental study we have performed provide evidences of the UP-resiliency relevance. They also show that (1) the order of application of the max-resolution steps has an impact on the UP-resiliency of the transformations and (2) the existing learning schemes do not capture all the UP-resilient transformations.

These results open several perspectives. Among them, it would be interesting to develop new max-resolution application orders to increase the percentage of UP-resiliency of the transformations. The existing learning schemes can also be improved, either by finding a characterization of the UPresilient transformations which can be efficiently checked or by completing the set of patterns used in the current leaning schemes. Now that we have a better understanding of the behavior of the max-resolution transformations, we can consider applying learning not only in the sub-part of the search tree but also in the upper part. The expected benefits would be an even more incremental LB computation and a better consideration of the structural properties of the instances.

As shown in the Max-SAT Evaluations, 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 above may allow to guide the exploration of the search tree by using the information learned as it is done in modern SAT solvers [Marques-Silva and Sakallah, 1999; E´en and S¨orensson, 2003]. Thus, the UP-resiliency property presented in this paper may be a significant step towards the improvement of BnB solver performance on industrial instances.