Chu-Min Li

Zhenxing Xu

Jordi Coll

Felip Manyà

Djamal Habet

Kun He

Combining Clause Learning and Branch and Bound for MaxSAT

Keywords: 2012 ACM Subject Classification Software and its engineering → Constraints MaxSAT, Branch&Bound, CDCL Digital Object Identifier 10.4230/LIPIcs.CP.2021.38

Branch and Bound (BnB) is a powerful technique that has been successfully used to solve many combinatorial optimization problems. However, MaxSAT is a notorious exception because BnB MaxSAT solvers perform poorly on many instances encoding interesting real-world and academic optimization problems. This has formed a prevailing opinion in the community stating that BnB is not so useful for MaxSAT, except for random and some special crafted instances. In fact, there has been no advance allowing to significantly speed up BnB MaxSAT solvers in the past few years, as illustrated by the absence of BnB solvers in the annual MaxSAT Evaluation since 2017. Our work aims to change this situation and proposes a new BnB MaxSAT solver, called MaxCDCL, by combining clause learning and an efficient bounding procedure. The experimental results show that, contrary to the prevailing opinion, BnB can be competitive for MaxSAT. MaxCDCL is ranked among the top 5 solvers of the 15 solvers that participated in the 2020 MaxSAT Evaluation, solving a number of instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best existing solvers, solves the highest number of instances of the MaxSAT Evaluations.

Introduction

The Maximum satisfiability problem (MaxSAT) is an optimization version of a well-studied and canonical NP-Complete problem, the satisfiability problem (SAT). Although SAT and MaxSAT share many aspects, solving MaxSAT is much harder than solving SAT in practice.

Indeed, since several clauses can be falsified in an optimal MaxSAT solution, some fundamental SAT techniques such as unit propagation cannot be used in MaxSAT as they are used in SAT. Despite this difficulty, huge efforts made by researchers make it possible nowadays to solve many interesting real-world and academic NP-hard optimization problems encoded as MaxSAT instances [START_REF] Bacchus | Maximum satisfiability[END_REF][START_REF] Chu | MaxSAT, hard and soft constraints[END_REF]. For this reason, MaxSAT has attracted increasing interest from the academy and industry in recent years.

As for many NP-hard problems, algorithms for MaxSAT are divided into two categories: exact algorithms, which return optimal solutions and prove their optimality; and heuristic algorithms, which quickly find solutions of good quality without guaranteeing their optimality. This paper will focus on exact algorithms for (unweighted) MaxSAT.

We roughly distinguish two types of exact algorithms for MaxSAT: branch-and-bound (BnB) algorithms [START_REF] Chu | MaxSAT, hard and soft constraints[END_REF], which directly tackle MaxSAT with a bounding procedure, but without unit propagation and clause learning; and SAT-based algorithms [START_REF] Bacchus | Maximum satisfiability[END_REF], which transform MaxSAT into a sequence of SAT instances and call a CDCL (Conflict-Driven Clause Learning) SAT solver to solve them. The performance of SAT-based MaxSAT algorithms is usually much better than BnB MaxSAT solvers in solving many real-world NP-hard optimization problems, because they indirectly exploit clause learning via the SAT solver. Unfortunately, it is hard for a BnB solver to exploit clause learning. In a CDCL SAT solver, a backtracking happens only when a clause is falsified, from which a sequence of resolution steps is performed to learn a clause explaining the backtracking. However, a BnB MaxSAT solver also need to backtrack when it computes a lower bound equal to the upper bound. In this case, no clause is explicitly falsified, making it hard to learn a clause. Probably because of this difficulty, there has been no advance allowing to significantly speed up BnB MaxSAT solvers in recent years, as illustrated by their absence in the annual MaxSAT Evaluation since 2017.

In this paper, we propose an original approach that allows a BnB MaxSAT solver to learn a clause when it computes a lower bound equal to the upper bound, together with a new bounding procedure, because the one in current BnB MaxSAT solvers is not adequate for large instances. This approach is implemented in a new BnB MaxSAT solver, called MaxCDCL, that combines the new bounding procedure and clause learning. The experimental results show that MaxCDCL is ranked among the top 5 solvers of the 15 solvers that participated in the 2020 MaxSAT Evaluation, solving a number of instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best existing solvers, solves the highest number of instances of the MaxSAT Evaluations.

Combining clause learning and BnB, as clause learning itself, belongs to the general framework consisting in explaining a failure in the search to avoid the same failure in the future. In other fields such as Pseudo-Boolean Optimization (PBO), there are also works in this framework (e.g. [START_REF] Devriendt | Learn to relax: Integrating 0-1 integer linear programming with pseudo-boolean conflict-driven search[END_REF]). The general framework is not hard to understand. However, making it effective for solving a particular problem such as SAT or MaxSAT is quite challenging, because this requires a deep understanding of the problem and the related solving techniques. So, one important contribution of our work is that we found a configuration and an efficient implementation of this configuration allowing to make the combination of clause learning and BnB effective for MaxSAT, as presented in this paper.

More importantly, our results refute a prevailing opinion in the field stating that, although BnB is a powerful technique that has successfully been used to solve many combinatorial optimization problems, it is not so useful for MaxSAT. Indeed, as the first BnB MaxSAT solver successfully exploiting clause learning, MaxCDCL opens promising research directions.

This paper is organized as follows: Section 2 presents the preliminaries. Section 3 reviews state-of-the-art MaxSAT solvers. Section 4 describes MaxCDCL. Section 5 empirically evaluates and analyzes MaxCDCL. Section 6 concludes.

Preliminaries

A propositional variable x can take values 0 or 1 (false or true). A literal is a variable x or its negation ¬x. A clause is a disjunction of k literals l 1 ∨ • MaxSAT is the problem of finding an assignment that satisfies the maximum number of clauses in a given multiset of clauses. In partial MaxSAT, there are hard and soft clauses, and the goal is to satisfy all the hard clauses and the maximum number of soft clauses. In weighted (partial) MaxSAT, each soft clause has a cost to pay if it is violated. This paper will focus exclusively on unweighted (partial) MaxSAT.

The state-of-the-art SAT solvers implement the CDCL algorithm. CDCL alternates a search phase, where literals are assigned until either a solution or a conflict is found, and a learning phase, which is executed after finding a conflict in order to learn a new clause. Unit Propagation (UP) is the main inference rule applied during the search: If there is a unit clause {l} in ϕ, literal l must be satisfied (i.e., set to 1). Then, any clause containing l is removed from ϕ, and all the occurrences of ¬l in clauses of ϕ are (implicitly) removed. UP is applied during the search until an empty clause (conflict) is found or no unit clause exists in ϕ. If UP finishes without finding a conflict, a new literal is picked following a heuristic and is set to 1 (we make a decision), and UP is applied again. If all the variables are assigned without finding a conflict, ϕ is satisfiable. The decision level of an assigned literal is the number of decisions made before being assigned. When a conflict is found, a conflict analysis is performed on the implication graph to derive a new clause explaining the conflict. Figure 1 shows an example of implication graph. It is a directed acyclic graph where each node represents an assignment l@dl, where l is a literal set to 1 and dl is its decision level. The negations of the literals of incoming edges of a node l@ld represent the reason (clause) why UP has set l = 1. For instance, node x 12 @5 is propagated due to clause ¬x 6 ∨ ¬x 4 ∨ x 12 (i.e., x 6 ∧ x 4 → x 12 ), given that x 4 and x 6 have been set to 1. A node without incoming edges represents a decision. All decisions are painted in grey, and the last one is dashed. A conflicting clause is represented by incoming edges to □; in this example, clause ¬x 3 ∨ ¬x 35 . A Unique Implication Point (UIP) is a node of the implication graph that belongs to all paths from the last decision to the conflict. Figure 1 contains three UIPs: the last decision x 4 , and literals x 13 and x 25 . The most used learning schema in CDCL SAT solvers is called first UIP (1UIP), guided by the closest UIP to the conflict in the implication graph.

When a conflict is found in the decision level dl (i.e., dl decisions were made before the conflict is found), a node in the decision level dl is said active if it is not the 1UIP but is in a path from the 1UIP to the conflict. In other words, the active nodes are those nodes that allow to reach the conflict from the 1UIP in the decision level dl. For example, in Figure 1, a conflict is found in the decision level 5, and x 3 @5 and x 35 @5 are active nodes. The 1UIP learning schema identifies, in each path from a node in a decision level lower than dl to an active node, the last literal in the lower decision level. The new learnt clause is composed of the negation of these literals and the 1UIP. For instance, in Figure 1, clause ¬x 8 ∨ x 11 ∨ ¬x 25 is learnt, because there are two paths from lower decision levels to an active node, in which x 8 and ¬x 11 are the last literals in lower decision levels, respectively. The learnt clause explains the conflict: when all its literals are falsified, unit propagation reproduces the implication graph to derive the same conflict. So, adding the learnt clause prevents the same conflict in the future search. After learning a clause, CDCL backtracks to the second highest decision level of the learnt clause (level 4 in the above example). Unsatisfiability is determined when a conflict is found at decision level 0.

Related Work

A major difference between MaxSAT and SAT solvers is that each clause must be satisfied in a SAT solution while a soft clause can be falsified in an optimal MaxSAT solution, making MaxSAT much harder to solve than SAT in practice. Despite this, the MaxSAT community has made huge efforts to implement exact MaxSAT solvers with impressive performance over the last decade [START_REF] Bacchus | Maximum satisfiability[END_REF][START_REF] Chu | MaxSAT, hard and soft constraints[END_REF]. On the other hand, heuristic MaxSAT algorithms such as SatLike [START_REF] Lei | Solving (Weighted) Partial MaxSAT by dynamic local search for SAT[END_REF] have also been proposed.

Roughly speaking, we find two main groups of exact MaxSAT solvers: branch-and-bound (BnB) and SAT-based solvers. BnB MaxSAT solvers implement the branch-and-bound scheme and incorporate a lookahead procedure that detects inconsistent subsets of soft clauses by applying unit propagation and computes a lower bound [START_REF] Chu | MaxSAT, hard and soft constraints[END_REF]. They also apply some inference rules at each node of the search tree. Representative BnB solvers are MaxSatz [START_REF] Chu | New inference rules for Max-SAT[END_REF], MiniMaxSat [START_REF] Heras | MiniMaxSAT: An efficient Weighted Max-SAT solver[END_REF], Ahmaxsat [START_REF] Abramé | Ahmaxsat: Description and evaluation of a branch and bound Max-SAT solver[END_REF][START_REF] Sami Cherif | Understanding the power of Max-SAT resolution through UP-resilience[END_REF] and Akmaxsat [START_REF] Kuegel | Improved exact solver for the Weighted MAX-SAT problem[END_REF]. Closely related to MaxSAT, we can find BnB solvers for the Weighted Constraint Satisfaction Problem (WCSP). Recently, it was presented a technique to improve BnB WCSP solving by avoiding branching on variables which are unlikely to increase the lower bound [START_REF] Trösser | Relaxation-aware heuristics for exact optimization in graphical models[END_REF].

SAT-based MaxSAT solvers proceed by reformulating the MaxSAT optimization problem into a sequence of SAT decision problems [START_REF] Bacchus | Maximum satisfiability[END_REF]. These solvers could still be divided into three subgroups: model-guided, core-guided and Minimum Hitting Sets (MHS-)guided. Model-guided approaches reduce to SAT the problem of deciding whether there exists an assignment for the MaxSAT instance with a cost less than or equal to a certain k, and successively decrease k until an unsatisfiable SAT instance is found. Among such solvers we find SAT4J-Maxsat [START_REF] Le | The Sat4j library, release 2.2[END_REF], QMaxSat [START_REF] Koshimura | QMaxSAT: A Partial Max-SAT solver[END_REF][START_REF] Zha | QMaxSAT in MaxSAT Evaluation[END_REF], Open-WBO [START_REF] Martins | Open-WBO: A modular MaxSAT solver[END_REF] or Pacose [START_REF] Paxian | Pacose: An iterative SAT-based MaxSAT solver[END_REF]. Core-guided and MHS-guided approaches consider a MaxSAT instance as a SAT instance and call a CDCL SAT solver to identify an unsatisfiable subset of soft clauses, called a core. Then, they relax this core and solve the relaxed instance with a CDCL SAT solver to identify another core, repeating this process until deriving a satisfiable instance. The difference between them is that core-guided solvers relax a core using cardinality constraints, while MHS-guided solvers remove one clause from each detected core so that the number of different clauses removed from the cores is minimized by solving a minimum hitting set instance with an integer programming solver. The most representative core-guided solvers include msu1.2 [START_REF] Marques | Towards more effective unsatisfiability-based maximum satisfiability algorithms[END_REF], WBO [START_REF] Vasco | Algorithms for weighted Boolean optimization[END_REF], Open-WBO [START_REF] Martins | Open-WBO: A modular MaxSAT solver[END_REF], WPM1 [START_REF] Ansótegui | Solving (Weighted) Partial MaxSAT through satisfiability testing[END_REF], PM2 [START_REF] Ansótegui | SAT-based MaxSAT algorithms[END_REF], WPM2 [START_REF] Ansótegui | A new algorithm for weighted partial MaxSAT[END_REF], WPM3 [START_REF] Ansótegui | WPM3: An (in)complete algorithm for Weighted Partial MaxSAT[END_REF], Eva [START_REF] Narodytska | Maximum satisfiability using core-guided MaxSAT resolution[END_REF], RC2 [START_REF] Ignatiev | RC2: an efficient maxsat solver[END_REF], and the most representative MHS-guided solvers include MHS [START_REF] Saikko | LMHS: A SAT-IP hybrid MaxSAT solver[END_REF] and MaxHS [START_REF] Bacchus | MaxHS in the 2020 MaxSAT Evaluation[END_REF][START_REF] Bacchus | Reduced cost fixing in MaxSAT[END_REF][START_REF] Davies | Solving MAXSAT by solving a sequence of simpler SAT instances[END_REF][START_REF] Davies | Exploiting the power of MIP solvers in MAXSAT[END_REF]. Core-guided search has also been extended to constraint programming [START_REF] Gange | Core-guided and core-boosted search for CP[END_REF].

A common point of SAT-based MaxSAT solvers is that they indirectly exploit the clause learning technique by repeatedly calling a CDCL SAT solver. Unfortunately, it is hard for BnB solvers to exploit clause learning, which might explain their poor performance on real-world optimization problems. We are aware of only one tentative in [START_REF] Abramé | Learning nobetter clauses in Max-SAT branch and bound solvers[END_REF]: when the number of falsified soft clauses reaches the upper bound, the falsification of these soft clauses is analyzed to learn a clause. Nevertheless, no clause is learnt when the lookahead procedure returns a lower bound equal to the upper bound, and the reported results are not competitive.

MaxCDCL: A BnB Algorithm Using CDCL for MaxSAT

This section first presents the general structure of MaxCDCL, and then the different components of our approach implemented in MaxCDCL.

General Structure of MaxCDCL

We distinguish between hard and soft conflicts in the MaxSAT context. A hard conflict occurs when the current partial assignment falsifies a hard clause. Given an upper bound UB, a soft conflict occurs when the current partial assignment cannot be extended to a complete one falsifying fewer than UB soft clauses. A CDCL SAT solver only considers hard conflicts, learns a hard clause from each hard conflict and backtracks. A BnB CDCL MaxSAT solver extends the CDCL SAT solver by also learning a hard clause from each discovered soft conflict and backtracks. Algorithm 1 depicts such a BnB CDCL MaxSAT solver called MaxCDCL. Given a MaxSAT instance with a set of hard clauses and a set of soft clauses, MaxCDCL works with H and S, where H contains the hard clauses and S contains a new literal y for each soft clause sc after adding the hard clauses encoding y ↔ sc to H. We call such y soft literal, because it represents a soft clause (i.e., a soft literal is satisfied if and only if the corresponding soft clause is satisfied). To solve the MaxSAT instance, MaxCDCL is repeatedly called with UB= 2 0 , 2 1 , 2 2 , 2 3 , . . . without exceeding |S| + 1 or UB f + 1 where UB f is a feasible upper bound computed by a heuristic solver with a short cutoff. This process stops when it obtains an assignment satisfying all clauses in H and falsifying fewer than UB soft literals in S. After that, MaxCDCL is repeatedly called with UB set to the number of falsified soft literals in the previous call, until no better solution can be found.

MaxCDCL is like a CDCL SAT solver except for two points. First, when UP does not falsify any hard clause in the UPLA procedure, it calls, under certain condition, a lookahead (LA) procedure to compute a lower bound |cores| of the number of soft literals that will be falsified if the current partial assignment is extended. If a soft conflict is discovered, i.e., if |f alseS| + |cores| ≥UB, it is analyzed to learn a clause for backtracking. Second, if no soft conflict is discovered, but it is discovered that the falsification of any free soft literal y not used in |cores| would result in a soft conflict, y is satisfied by a procedure called hardening.

Note that model-guided MaxSAT solvers also set a UB in their search. However, they do not compute a lower bound to discover soft conflicts as MaxCDCL. Consequently, MaxCDCL is able to backtrack much earlier than model-guided MaxSAT solvers for a given UB. See the next subsection for details and illustrative examples.

24

H ← H ∪ {l} where l is a free literal selected using a heuristic;

Combining Lookahead and Clause Learning

A subset of soft literals S i = {y 1 , . . . , y |Si| } is inconsistent if they cannot be simultaneously satisfied. This inconsistency can be represented by the hard clause

¬y 1 ∨ • • • ∨ ¬y |Si| . Note that |S i | can be 1.
If the inconsistency is independent of any partial assignment, the subset is called a global core. Otherwise, the inconsistency is implied by a subset of literals and the inconsistent subset of soft literals is called a local core. The core-guided or MHS-guided SAT-based MaxSAT solvers only detect global cores to relax them, while our approach detects local cores, given a partial assignment, to discover a soft conflict.

▶ Example 1. Let H = {¬y 1 ∨x 1 ∨¬x 2 , ¬x 1 ∨¬x 3 ∨¬x 4 , ¬y 2 ∨x 3 , ¬y 3 ∨x 5 }, where y 1 , y 2 and y 3 are soft literals. If no variable is assigned, all soft literals can be simultaneously satisfied. So, no global core exists. However, if the current partial assignment is {x 2 = 1, x 4 = 1}, the subset of soft literals {y 1 , y 2 } is a local core implied by the partial assignment. We write the implication by H ∪ {x 2 , x 4 } → ¬y 1 ∨ ¬y 2 .

Proposition 2 provides the foundation of our approach in the general case.

▶ Proposition 2. Let H be a set of hard clauses, S = {y 1 , . . . , y |S| } be the set of all soft literals, k be an integer, and

L i = {l i1 , . . . , l i|Li| } (1 ≤ i ≤ k) be a set of literals. If, for every i (1 ≤ i ≤ k), H ∪ L i implies a local core S i = {z i1 , . . . , z i|Si| } ⊂ S (i.e., H ∪ L i → ¬z i1 ∨ • • • ∨ ¬z i|Si| )
, and S i and S j are disjoint for any j ̸ = i such that 1 ≤ j ≤ k, then every assignment that satisfies

H ∪ {¬y 1 + • • • + ¬y |S| < k} also satisfies the clause ¬l 11 ∨ • • • ∨ ¬l 1|L1| ∨ • • • ∨ ¬l k1 ∨ • • • ∨ ¬l k|L k | . Proof. It is easy to see that H ∪ L 1 ∪ • • • ∪ L k implies (¬z 11 ∨ • • • ∨ ¬z 1|S1| ) ∧ • • • ∧ (¬z k1 ∨ • • • ∨ ¬z k|S k | ), meaning that H ∪ L 1 ∪ • • • ∪ L k falsifies the constraint ¬y 1 + • • • + ¬y |S| < k, because each clause ¬z i1 ∨ • • • ∨ ¬z i|Si| implies at least one different falsified soft literal. Hence, any assignment satisfying H ∪ {¬y 1 + • • • + ¬y |S| < k} must falsify at least one literal in L 1 ∪ • • • ∪ L k , and satisfy the clause ¬l 11 ∨ • • • ∨ ¬l 1|L1| ∨ • • • ∨ ¬l k1 ∨ • • • ∨ ¬l k|L k | .
Note that we use "z" (instead "y") to denote a soft literal in a local core to avoid complex subscripts. ◀ Given a partial assignment F of H, the application of Proposition 2 consists in first detecting a local core S i and then identifying the smallest L i ⊂ F such that H ∪ L i implies S i . We call L i the reason of S i . If k is the current upper bound UB and k disjoint local cores are detected, a soft conflict is discovered, and the clause

¬l 11 ∨• • •∨¬l 1|L1| ∨• • •∨¬l k1 ∨• • •∨¬l k|L k | , which is implied by H ∪{¬y 1 +• • •+¬y |S| < k}
and is falsified by the current partial assignment, can be considered by an implicit clause explaining the soft conflict. This clause can be further analyzed using the 1UIP schema in line 10 of Algorithm 1 to learn a clause to be explicitly added to H to prevent the same soft conflict in the future as in the hard conflict case.

The detection of a local core S i is implemented by using UP in a lookahead procedure as in existing BnB MaxSAT solvers [START_REF] Chu | Resolution-based lower bounds in MaxSAT[END_REF]28,[START_REF] Chu | Detecting disjoint inconsistent subformulas for computing lower bounds for Max-SAT[END_REF]. The advantage of this procedure is that S i is minimal w.r.t. UP, in the sense that UP cannot detect any local core that is a proper subset of S i under the same partial assignment [START_REF] Chu | Resolution-based lower bounds in MaxSAT[END_REF], which is essential for our approach, because MaxCDCL needs to learn clauses of good quality from the detected local cores. Recall that BnB MaxSAT solvers detect disjoint local cores but do not explain them. When a soft conflict is discovered, they simply backtrack without learning a hard clause from the soft conflict, which is very different from MaxCDCL.

Concretely, MaxCDCL calls Algorithm 2 at decision level dl with a partial assignment F , under which the already falsified soft literals are stored in a set named f alseS. The lookahead procedure starts at line 5 in Algorithm 2 when no hard conflict is found, and terminates at line 10 or line 24. This procedure proceeds in decision level dl+1 by maintaining a set of detected local cores (cores). Every iteration of the loop (line 8) propagates a free soft literal y not occurring in cores, until a clause h in H is falsified or a soft literal sl not occurring in cores is falsified (line 13). These unit propagations construct an implication graph G. The propagated free soft literals y 1 , y 2 , . . . in the loop can be seen as temporary assumptions at decision level dl+1 that have no incoming edge in G.

Inspecting G, let z 1 , . . . , z b be the subset of literals y 1 , y 2 , . . . at level dl+1 and without incoming edge, from which there is a path to h or to ¬sl. Then, {z 1 , . . . , z b } (resp. {z 1 , . . . , z b , sl}) is a local core S i implied by the partial assignment F at decision level dl. Based on G, we can also define L i as the set containing, from each path to h (resp. ¬sl), the last literal assigned before level dl + 1. Clearly,

H ∪ L i implies ¬z 1 ∨ . . . ∨ ¬z b (resp. ¬z 1 ∨ . . . ∨ ¬z b ∨ ¬sl).
Note x2@2 y1@5 y2@5 x1@3 ¬x3@5 x4@3 ¬y3@5 A)

¬l 1|L1| ∨ • • • ∨ ¬l k1 ∨ ¬l k2 ∨ • • • ∨ ¬l k|L k | could
x1@3 y4@5 y5@5 x5@4 x2@2 x7@5 x4@3 x8@5 y2@5 x6@5 y6@5 B)

Figure 2 Implication graphs involved in the detection of cores in Example 3. Grey nodes represent decisions or assumptions, and dashed nodes represent assignments made in the lookahead process.

After propagating y 1 , y 2 is satisfied and y 3 is falsified. Hence sl=y 3 is detected, the implication graph in Figure 2A is obtained, looking at which core={y 1 , y 3 } will be identified at line 18 with reason={x 2 , x 4 }, because there are paths from x 2 and x 4 to ¬y 3 , and the next literals to x 2 and x 4 in the paths are from decision level 5.

Note that since y 2 is not in cores, it can be used to detect new cores. After propagating y 2 , y 4 , y 5 , the implication graph of Figure 2B

∨ • • • ∨ ¬l 1|L1| ∨ • • • ∨ ¬l k1 ∨ • • • ∨ ¬l k|L k | .
Note that this hardening satisfies a fundamental requirement of CDCL SAT solvers: except the decision (i.e., branching) variables, the value of every variable must be explicitly associated with a reason. In contrast, although existing BnB MaxSAT solvers also implement hardening, no reason is associated with the hardening.

Let m = |H| + |S|. UP is in O(m) for detecting one local core. Since the lookahead procedure detects at most UB cores, its whole complexity is in O(m×UB).

A Probing Strategy for Lookahead

Existing BnB MaxSAT solvers usually tackle random or crafted instances of limited size and look ahead at each branch. However, such a treatment might be too costly and useless for large instances. If the lower bound is not tight enough to prune the current branch, the time spent to compute the lower bound is lost. When k = UB-|f alseS|, the lookahead procedure has to detect k disjoint local cores to be successful. Generally, the greater the value of k, the lower the probability of lookahead to be successful.

MaxCDCL uses a probing strategy to determine if lookahead has to be applied at the current branch. With probability p, where p is a parameter intuitively fixed to 0.01, lookahead is applied for probing purpose. The mean avgp and the standard deviation devp of the number of detected disjoint local cores in a successful probing lookahead are computed (not shown here due to the lack of space) to select the branches where lookahead is applied.

C P 2 0 2 1 38:10 Combining Clause Learning and Branch and Bound for MaxSAT

Inspired by the 68-95-99.7 rule in statistics, which says that the values within one (two, three) standard deviation of the mean account for about 68% (95%, 99.7%) of a normal data set, we reasonably assume that the number of cores detected in a successful lookahead is probably lower than avgp + coef * devp when coef = 3. So, lookahead is not applied at the current branch when k > avgp + coef * devp. However, since the probing may not get exact information and the values may not follow a perfect normal distribution, coef is dynamically adjusted to maintain the success rate of lookahead between lowRate and highRate, where lowRate and highRate are parameters intuitively fixed to 0.6 and 0.75, respectively.

Concretely, coef is initialized to 2 for each UB. At each probing, if the success rate of lookahead since the last probing is greater than highRate, it is increased by 0.1; and if it is lower than lowRate, it is decreased by 0.1. There are no lower and upper bounds on coef . When it is too low so that no lookahead is performed between two probings, it is reset to 2.

Soft literal ordering in lookahead

Existing BnB MaxSAT solvers such as MaxSatz usually propagate soft unit clauses in the ordering these clauses become unit, or in their ordering in the input formula when detecting disjoint cores [28]. MaxCDCL propagates first the soft literals in the cores detected in the previous lookahead. We use this ordering for two intuitive reasons.

Before backtracking, a local core detected in the previous lookahead remains to be a core. Re-detecting a previous local core allows to obtain a possibly smaller local core due to additional assignments. After backtracking, re-detecting local cores in the previous soft conflict may allow to detect a new soft conflict sharing many local cores with the previous conflict. In this way, the clauses learnt from consecutive soft conflicts allow to intensify the search, because the clause learnt from a soft conflict is derived from the reasons of the detected cores.

The quality of a clause learnt from a soft conflict highly depends on the detected cores, which in turn highly depends on the soft literal ordering. How to improve the quality of the learnt clause by further improving the soft literal ordering definitely deserves future study.

Improving the VSIDS heuristic by lookahead

When there is no unit clause, a CDCL SAT solver chooses a free literal l using a decision heuristic, satisfies l and then performs unit propagation. VSIDS [START_REF] Moskewicz | Chaff: Engineering an efficient SAT solver[END_REF] is one of the widely used decision heuristics: it initializes the score of each variable to 0, and then at each conflict, it increases the score of each variable in a path to the conflict in the implication graph by var_inc, where var_inc is initialized to 1 and, after each conflict, it is divided by a parameter usually set to 0.95 to give more importance to the next conflict. Note that VSIDS is a heuristic based on lookback, because it is based on the conflicts in the past.

VSIDS is also used in MaxCDCL by increasing the score of a variable in a soft or hard conflict as in a CDCL SAT solver, but is modified as follows by taking lookahead into account. Every time the lookahead procedure detects a local core, the score of the variables encountered when identifying the reason of the core (see Subsection 4.2) is increased by var_inc × γ, where γ is a discount-rate parameter as in reinforcement learning, and is empirically fixed to 0.1. The intuition of this modification is the following. A soft conflict is derived when UB local cores are detected. So a variable contributing to many local cores should be favoured to reach a soft conflict as early as possible. However, a local core represents only a component of a future possible soft conflict but not a soft conflict for sure. So the increase of the score of a variable contributing to a core should be discounted by γ.

Implementation of MaxCDCL

Since MaxCDCL can be considered as an extension of a CDCL SAT solver, it is implemented on top of the CDCL SAT solver MapleCOMSPS_LRB [START_REF] Hui Liang | Proceedings of SAT Competition 2016: Solver and Benchmark Descriptions[END_REF], winner of the application track of SAT competition 2016. We chose MapleCOMSPS_LRB because it was one of the best SAT solvers with deterministic behavior when we started this work in 2017. Nevertheless, some of the recent advances in SAT solving are incorporated, including1 :

The approach from [START_REF] Li | Clause vivification by unit propagation in CDCL SAT solvers[END_REF][START_REF] Luo | An effective learnt clause minimization approach for CDCL SAT solvers[END_REF] is applied to minimize the learnt clauses.

The clause size reduction with the all-UIP learning technique from [START_REF] Feng | Clause size reduction with all-uip learning[END_REF] is applied to reduce the clauses learnt from soft conflicts. This technique is particularly useful for MaxCDCL, because a clause learnt from a soft conflict is usually longer than a clause learnt from a hard conflict. The all-UIP technique allows to significantly reduce the size of a clause learnt from a soft conflict.

The learnt clause management technique proposed in [START_REF] Kochemazov | Improving implementation of SAT competitions 2017-2019 winners[END_REF] is incorporated into MaxCDCL, allowing more learnt clauses to be kept in the clause database.

In addition, let S = {y 1 , . . . , y |S| } be the set of all soft literals. When |S| × (UB-1) ≤ 10 4 , the sequential SAT encoding [START_REF] Sinz | Towards an optimal CNF encoding of Boolean cardinality constraints[END_REF] of the cardinality constraint ¬y 1 + ¬y 2 + • • • + ¬y |S| <UB is added to the input instance before starting the search. MaxCDCL alternates LRB phases and VSIDS phases for its search as MapleCOMSPS_LRB, using the LRB heuristic and the VSIDS heuristic modified as in subsection 4.5, respectively. Each phase is limited to a number of unit propagations specified by the parameter phaseLength, which is initialized to 2 × 10 7 and is doubled every cycle of LRB phase and VSIDS phase. In the VSIDS phase, the glucose restart strategy [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF] is used; in the LRB phase, the Luby restart strategy [START_REF] Luby | Optimal speedup of Las Vegas algorithms[END_REF] is used.

We plan to implement MaxCDCL on top of Kissat [START_REF] Biere | Paracooba, Plingeling and Treengeling entering the SAT Competition[END_REF], the winner of the SAT2020 competition, which might further improve its performance.

Experimental Evaluation

We report on an experimental investigation to assess the performance of MaxCDCL. We ran all experiments with Intel Xeon CPUs E5-2680@2.40GHz under Linux with 32GB of memory, using the following benchmark sets, unless otherwise stated:

MSE19∪20:

The union of all the instances used in the complete unweighted track of the MaxSAT Evaluations (MSE) 2019 and 2020, a total of 1000 distinct instances. MC: A subset of the Master Collection of instances from the MaxSAT evaluations held until 20192 . It contains 16080 unweighted (partial) MaxSAT instances, classified into 51 families and 76 subfamilies. MC includes all the instances of the 63 subfamilies having 100 instances or less, and the first 100 instances as they occur in the natural order in each of the remaining 13 subfamilies, considering a total of 3614 instances. This selection provides a simple, deterministic and objective criterion that does not favor any solver; and the experiments can be easily reproduced. MC contains 726 instances that also belong to MSE19∪20.

The cutoff time is one hour (3600s) per instance as in the MaxSAT Evaluation. For MaxCDCL and its variants, this includes 60 seconds to find a feasible upper bound UB f with SatLike (version 3.0). Note that MaxCDCL and its variants do not start the search from UB=UB f , but from 0 , then 2 1 , 2 2 , . . . , until a feasible solution is found or 2 i > UB f . In the latter case, UB is set to UB f + 1. Then, UB is gradually decreased until no better solution can be found (see Section 4.1).

The experiments are presented as follows. Firstly, we analyse the impact of the components implemented in MaxCDCL. Secondly, we compare the performance of MaxCDCL with that of the top 5 solvers in MSE2020. Thirdly, we show the complementarity of MaxCDCL with the top 5 solvers by comparing the number of instances solved using a portfolio solver with and without MaxCDCL. Finally, we compare MaxCDCL with a state-of-the-art BnB solver.

MaxCDCL Components

Table 1 compares MaxCDCL with the following variants:

MaxCDCL\LA. MaxCDCL without lookahead, i.e. the condition to lookahead is never satisfied in line 3 of Algorithm 2. Note that after finding a feasible UB, MaxCDCL\LA performs linear SAT-UNSAT search as a model-guided SAT-based MaxSAT solver. MaxCDCL\harden. MaxCDCL without hardening (i.e., lines 17 and 18 in Algorithm 1 are removed). MaxCDCLalwaysLA. MaxCDCL that looks ahead at every branch, i.e., the condition to lookahead is always satisfied in line 3 of Algorithm 2. MaxCDCLioLA. MaxCDCL that, when detecting cores in lookahead, always propagates the soft literals in the ordering as the corresponding soft clauses occur in the input instance. MaxCDCL\VSIDSbyLA. MaxCDCL that does not increase the VSIDS score of the variables contributing to a local core detected in lookahead as described in Subsection 4.5.

In Table 1, columns "#solv" give the number of solved instances and columns "avg" give the mean time in seconds (including the 60s used by SatLike) needed to solve these instances. These results indicate that a careful configuration combining clause learning and BnB is crucial for the performance of MaxCDCL, including: hardening based on local core detection and clause learning, the selective and adaptive application of lookahead and the ordering to propagate the soft literals when detecting local cores, because the absence of any of these components makes a significant number of instances out of reach of MaxCDCL. Without this configuration, MaxCDCL\LA solves 229 instances less than MaxCDCL in MES19∪20 and 839 instances less than MaxCDCL in MC. Note that although the hardening of a soft literal requires a distinct learnt clause, it does not increase the total memory usage, because it allows to avoid many learnt clauses by reducing search space.

Recall that the most fundamental feature of MaxCDCL is the clause learning from soft conflicts. We computed the average length of a clause learnt from a soft (hard) conflict for each solved instance by MaxCDCL in MSE19∪20, and found that the median average length In addition, the comparison of MaxCDCL with MaxCDCL\VSIDSbyLA suggests that the VSIDS heuristic might be improved by lookahead, indicating a promising research direction.

To complete the subsection, we mention the impact of two other components of MaxCDCL: (1) the local search by SatLike in preprocessing to compute a feasible UB allows MaxCDCL to solve 8 more instances in MSE19∪20; (2) the sequential cardinality constraint encoding is applied to about the 20% of the instances in MSE19∪20 for at least one UB, helping solve 39 extra instances in MSE from highly symmetric problems such as drmx-at-most-k.

Comparison with the top 5 Solvers in MSE2020

A total of 15 solvers competed in the complete unweighted track of MSE2020 [START_REF] Bacchus | MaxSAT Evaluation 2020: Solver and benchmark descriptions[END_REF]. We consider the top 5 solvers: MaxHS (mhs in short), which is MHS-guided; EvalMaxSAT (eval in short), RC2-B (rc2 in short) and open-wbo-res-mergesat-v2 (Open-WBO or owbo in short), which are core-guided; and UWrMaxSAT (uwr in short), which combines both core-guided and model-guided solving. We executed the versions used in MSE2020 in all the experiments.

Table 2 shows the results for MSE19∪20 and MC, respectively. Column "#uniq" has the number of instances that were only solved by the solver in the row. Column "#win" has the number of instances solved by MaxCDCL but not by the solver in the row.

We observe that MaxCDCL solves more instances than two top 5 solvers in MSE19∪20 and four top 5 solvers in MC. More importantly, MaxCDCL solves a significant number of instances that other solvers cannot solve. For example, MaxCDCL solves 116 instances in MC that MaxHS does not solve. If we consider all the solvers together, there is also a significant number of instances solved by MaxCDCL that no other solver is able to solve: 16 instances in MSE19∪20 and 67 instances in MC that mainly come from the subfamilies MaxClique, MaxCut and UAQ. These results show that the existing MaxSAT solvers, especially the model-guided and core-guided ones, are able to solve similar kinds of instances. Nevertheless, MaxCDCL has the potential to solve new kinds of instances that are not solvable with the current MaxSAT techniques. It is important to note that MaxCDCL is far from being as optimized as the other solvers, which are the result of a process of continuous improvements since more than ten years.

Combining MaxCDCL with existing solvers

Given two deterministic solvers X and Y and a time limit T to solve an NP-hard problem such as MaxSAT, the simplest way to try to solve more instances than X and Y alone within the time limit T is to combine X and Y by running X within the time limit T /2, and then Y from scratch within the remaining time T /2 if the instance is not solved by X.

C P 2 0 2 1

Table 3 Results for MSE19∪20 (left) and MC (right). The entry in cell (X, Y ) for X ̸ = Y is the number of instances solved by running solver X for 1800 seconds, and then solver Y from scratch for 1800 seconds if the instance is not solved by X. The entry in cell (X, X) (in the diagonal in grey) is the number of instances solved by running solver X for 1800 seconds. Column X in the last row recalls the results of solver X with 3600 seconds. Table 3 shows the results of all possible pairwise combinations of the top 5 solvers and MaxCDCL (mcdcl) in MSE2020 for T = 3600s. Each cell (X, Y ) for X ̸ = Y contains the number of instances solved by running solver X for 1800s and then solver Y from scratch for 1800s in MSE19∪20 (left) and MC (right). Each cell (X, X) (in the diagonal in grey) contains the number of instances solved by X in 1800s. Column X in the last row recalls the results of X with 3600 seconds. Combining any of the top 5 solvers with MaxCDCL solves more instances than this solver and MaxCDCL alone within 3600s, while this is not always true when combining two top 5 solvers. For example, combining MaxHS and Open-WBO solves 763 instances in MSE19∪20 within 3600s, while MaxHS alone solves 769 instances within 3600s. This shows that MaxCDCL is more complementary with the top 5 solvers than other solvers.

More importantly, MaxCDCL combined with the top 2 solvers, MaxHS and EvalMaxSAT, solves the highest numbers (785 and 786) of instances in MSE19∪20. This result is significantly better than that of MaxHS or EvalMaxSAT alone, and the best combination without MaxCDCL solves only 777 instances. The results are even more striking in MC, where the worst combination of MaxCDCL with a top 5 solver is better than any other combination not including MaxCDCL, and combining MaxHS and MaxCDCL gives the best results, solving 93 instances more than the previous best result achieved by MaxHS alone, and 57 instances more than the best combination without MaxCDCL.

Figure 3 shows cactus plots comparing the best two combinations of solvers with Max-CDCL, the best two combinations without MaxCDCL, as well as the best two mono-solvers, for MSE19∪20 (left) and MC (right). Other solvers and combinations are excluded for readability reasons. For any time T (0 < T ≤ 3600s), a curve gives the number of instances solved by a mono-solver or a combination of two solvers within T , where the number of instances solved by a combination X-Y of solvers X and Y within T is the number of instances solved by running X for T /2, and then Y for T /2. The solving time of a combination X-Y of solvers X and Y for an instance is twice the minimum solving time among X and Y . This simulates a parallel execution of X and Y by alternating them in small time periods. The plots clearly show the advantage of combining an existing solver with MaxCDCL, allowing to solve the highest number of instances within 3600s, and the advantage becomes greater as the running time is increased.

Figure 3

Cactus plots of the best two combinations with MaxCDCL (mcdcl in short), the best two without MaxCDCL, and the best two mono-solvers for MSE19∪20 (left) and MC (right). For each point (N, T ) in a curve for a mono-solver X, N is the number of instances solved by X in T seconds; and for each point (N, T ) in a curve for a combination X-Y of solvers X and Y , N is the number of instances solved by running X for T /2 seconds followed by running Y for T /2 seconds. The names of the solvers and combinations are listed in the order of the highest points of the corresponding curves from left to right for readability.

Comparison with a BnB Solver

We compare MaxCDCL with ahmaxsat, which was the best BnB solver in the last MaxSAT evaluation (MSE2016) in which BnB solvers competed. We use the MSE2016 instances of the categories MaxSAT (ms) and partial MaxSAT (pms). Each category has random (ran), crafted (craf), and industrial (in) instances. Thus, we consider a total of 6 families.

The results are shown in Table 4, where the number of instances for each family is given in column "#ins". We observe that ahmaxsat solves more random and non-partial crafted instances. A learnt clause for these instances with randomness and limited size usually contains most of the variables of the instances and is hardly useful. So, the higher use of lower bounding methods and the lack of clause learning in ahmaxsat are adequate for them, and the higher use of lower bounding methods (like in MaxCDCLalwaysLA) does not improve MaxCDCL for them because of clause learning. However, ahmaxsat has poor performance on other instances. Instead, MaxCDCL solves a much higher number of such instances.

Conclusion

We described MaxCDCL, a MaxSAT solver that combines, for the first time to the best of our knowledge, branch and bound and clause learning. The main differences of MaxCDCL with existing SAT-based MaxSAT solvers are the following: The extensive experimentation conducted shows that MaxCDCL is ranked among the top 5 exact MaxSAT solvers in the 2020 MaxSAT evaluation. Furthermore, it solves a significant number of instances that other solvers cannot solve, suggesting that combining branch and bound and clause learning has the potential to solve new kinds of instances that are not solvable with current MaxSAT techniques. More importantly, combining MaxCDCL with the existing solvers allows to solve the highest number of MaxSAT instances.

C P 2
Detailed analyses indicate that the performance of MaxCDCL comes from a careful configuration combining clause learning and BnB, including hardening based on local core detection and clause learning, the selective and adaptive application of lookahead, and the ordering to propagate the soft literals when detecting local cores.

We believe that the proposed approach opens new and promising research directions, including for example: (1) improving the quality of the clauses learnt from soft conflicts by designing new soft literal orderings in lookahead; (2) exploiting the relationship of SAT and MaxSAT for improving SAT and MaxSAT solving; (3) adapting the approach of MaxCDCL to other problems such as pseudo-Boolean optimization and Max-CSP; (4) extending MaxCDCL to weighted MaxSAT, in which each soft clause is weighted. In the extension of MaxCDCL to weighted MaxSAT, each soft clause is represented by a weighted soft literal. A local core detected by lookahead is weighted by the minimum soft literal weight it contains, and other weights are split to be used in other core detections. When the total weight of all detected local cores reaches UB, a soft conflict is discovered. The challenge here is that there can be more local cores to detect than in the unweighted case. Thus, the clause learnt from a soft conflict can be longer. Special strategies in clause and soft literal ordering should be designed to learn shorter clauses from soft conflicts.

4 1UIPFigure 1

 41 Figure 1 Example of implication graph.

Algorithm 1 begin 2 while true do 3 currentLevel 4 while true do 5 ( 6 if 7 if currentLevel = 0 then 8 return UB; 9 else 10 newLearntClause 15 if all variables are assigned then 16 return |f alseS|; 17 else 18 hardening

 1234567891015161718 MaxCDCL(H, S,UB), a generic CDCL procedure with lookahead for MaxSAT. Input: H: a set of hard clauses, S: a set of soft literals, UB: an upper bound. Output: |f alseS|, where f alseS is the set of falsified soft literals, if |f alseS| <UB; or UB otherwise 1 ← 0; /* start or restart search */ cl, f alseS, cores, reasons) ← UPLA(H, S, UB, currentLevel); cl is a falsified hard clause or |f alseS| + |cores| ≥UB then ← analyze(cl, f alseS, reasons); 11 level ← the second highest level in newLearntClause; 12 backtrackTo(level); 13 currentLevel ← level; 14 else if |f alseS| + |cores| = UB-1 then

  • • ∨ l k . A propositional formula in Conjunctive Normal Form (CNF) is a conjunction (or a set) of m clauses c 1 , . . . , c m . An assignment of truth values to the propositional variables satisfies a literal x if x = 1, and satisfies a literal ¬x if x = 0. A literal x or ¬x is assigned if x is assigned a value, otherwise it is free. An assignment is complete if all the variables are assigned a value, otherwise it is partial. A (partial) assignment is usually represented by a (sub)set of satisfied literals. A clause is satisfied if at least one of its literals is satisfied. A CNF is satisfied if all its clauses are satisfied. The Boolean satisfiability (SAT) problem for a CNF ϕ is to determine whether there exists an assignment that satisfies ϕ.

C P 2 0 2 1 38:8 Combining Clause Learning and Branch and Bound for MaxSAT Algorithm 2

  that each already falsified soft literal y in f alseS constitutes a local core S i ={y} not in cores, implied by H ∪ {¬y} (i.e. L i ={¬y}). Therefore, when k = |f alseS| + |cores| = UB in MaxCDCL, we have UB disjoint local cores. According to Proposition 2, ¬l 11 ∨ • • • ∨ UPLA(H, S, UB, dl), Unit propagation followed by lookahead. H: a set of hard clauses, S: a set of soft literals, UB: an upper bound, dl: the current decision level. Output: cl: a hard clause; f alseS: the set of falsified soft literals; cores: a set of disjoint local cores; reasons: a set of literals that are reasons of cores 1 begin Increase the decision level to dl + 1;

	2	(cl, f alseS) ← UP(H);
	3	if cl is a falsified hard clause or |f alseS| ≥ UB or the condition to lookahead is
		not satisfied then
	4	return (cl, f alseS, ∅, ∅);
	5	H ′ ← H; F ← {¬l|l is falsified in H};
	6	reasons ← ∅; cores ← ∅; S ′ ← ∅;

Input: 7 8 while true do 9 if all soft literals of S either are non-free or occur in cores then 10 return (cl, f alseS, cores, reasons); 11 Let y be a free soft literal not occurring in cores; 12 H ← H ∪ {y}; S ′ ← S ′ ∪ {y}; 13 (h, sl) ← UPforLA(H) ; 14 if h is a falsified hard clause or sl a falsified soft literal not in cores then 15 if h is a falsified hard clause then 16 core ← {l|l ∈ S ′ and l has no incoming edge and there is a path from l to h in the implication graph}; 17 else 18 core ← {sl} ∪ {l|l ∈ S ′ and l has no incoming edge and there is a path from l to ¬sl in the implication graph}; 19 reason ← {l|l ∈ F and there is a path from l to h or ¬sl in the implication graph, and the literal next to l in the path is of decision level dl + 1}; 20 cores ← cores ∪ {core}; 21 reasons ← reasons ∪ reason; 22 H ← H ′ ; S ′ ← ∅; /*Cancel UP done by lookahead*/ 23 if |cores| + |f alseS| ≥ UB then 24 return (cl, f alseS, cores, reasons);

  be considered as an implicit clause in H, which is falsified by the current partial assignment and is analyzed using the 1UIP schema in line 10 of Algorithm 1 to learn a clause as in the hard conflict case. Let y 1 , . . . , y 7 be soft literals, and let H be formed by¬y 1 ∨ y 2 ∨ ¬x 2 ¬y 2 ∨ ¬x 3 ∨ ¬x 4 ¬y 2 ∨ ¬y 5 ∨ x 6 ¬x 1 ∨ x 4 ¬y 3 ∨ x 3 ¬x 6 ∨ ¬x 5 ∨ y 6 ¬y 6 ∨ ¬x 2 ∨ x 7 ¬x 7 ∨ ¬y 6 ¬y 4 ∨ x 8 ¬y 7 ∨ x 9If no variable is assigned, all soft literals can be simultaneously satisfied. So, no global core exists. Let the current partial assignment be {y 7 =0, x

▶ Example 3. 2 =1, x 1 =1, x 4 =1, x 5 =1}, where x 4 is propagated due to ¬x 1 ∨ x 4 , and the other literals have been decided. Hence f alseS = {y 7 } and the current decision level is 4. Let also UB=3. We show how Algorithm 2 detects cores and reaches UB by propagating the free soft literals y 1 , . . . , y 6 , by means of Figure

2

.

  is obtained, and a conflicting clause h={¬x 7 ∨ ¬y 6 } is detected. Then, core={y 2 , y 5 } is detected at line 16 with reason={x 2 , x 5 }.Since |cores| + |f alseS| = 2 + 1 = UB, a soft conflict is found at line 23, withreasons={x 2 , x 4 , x 5 , ¬y 7 }. According to Proposition 2, clause ¬x 2 ∨ ¬x 4 ∨ ¬x 5 ∨ y 7 is implied by H ∪ {¬y 1 + • • • + ¬y |S| < 3},which is falsified at decision level 4, and hence can be analysed with the 1UIP scheme at level 4 to learn a new clause and backtrack. Note that a model-guided MaxSAT solver would not discover this soft conflict at this stage, because UB=3 but only one soft literal is falsified. Proposition 2 also provides the basis for hardening. If k = |f alseS| + |cores| = UB-1, for each free soft literal z not in the k local cores, H ∪ {¬z} implies a new local core {z}. The hardening procedure (line 18 in Algorithm 1) satisfies z with the reason z ∨ ¬l 11

Table 1

 1 Comparison of MaxCDCL with its variants for MSE19∪20 (left) and MC (right).

		#solv	avg	#solv	avg
	MaxCDCL\LA	505 255s	2183 194s
	MaxCDCL\harden	664 281s	2878 194s
	MaxCDCLalwaysLA	681 249s	2962 193s
	MaxCDCLioLA	704 268s	2963 168s
	MaxCDCL\VSIDSbyLA	724 268s	3003 165s
	MaxCDCL	734 256s	3022 156s

Table 2

 2 Results for MSE19∪20 (left) and MC (right) with top 5 solvers. Note that the learnt clause length averaged across the 734 instances does not make sense because it is biased by few instances with very long learnt clause length.

		#solv	avg #uniq #win	#solv	avg #uniq #win
	MaxHS	769 177s	11	36	3037 85.5s	26	116
	EvalMaxSAT	759 129s	1	43	3002 69.7s	4	147
	UWrMaxSAT	745 128s	3	42	2969 51.6s	7	141
	RC2-B	728 164s	0	62	2948 70.1s	1	173
	Open-WBO	695 157s	3	71	2906 89.7s	4	190
	MaxCDCL	734 256s	16	-	3022	156s	67	-
	of a clause learnt from a soft (hard) conflict is 23.67 (19.2) among the 734 instances solved in
	the set.

  The best results are in bold.

		mhs	eval	uwr	rc2	owbo	mcdcl	mhs	eval	uwr	rc2	owbo	mcdcl
	mhs	747	777 777	770 763 785	3009	3068	3073	3056	3049 3130
	eval	777	745 760	751 760 786	3068	2972	3019	2986	3013 3126
	uwr	777	760 730	745 746	774	3073	3019	2951	3000	2998 3098
	rc2	770	751 745	713 745 778	3056	2986	3000	2921	2981 3105
	owbo	763	760 746	745 675	746	3049	3013	2998	2981	2865 3076
	mcdcl 785 786 774 778 746	711	3130 3126 3098 3105	3076	2992
	3600s	769	759 745	728 695	734	3037	3002	2969	2948	2906	3022

Table 4

 4 Results for MSE16 and MSE19∪20.

				ahmaxsat	MaxCDCL
			#ins #solv	avg #solv	avg #win
		ms_ran	454	259	744s	27 1535s	0
	MSE16	ms_craf ms_in pms_ran pms_craf	402 55 210 678	230 33.0s 0 -209 148s 369 242s	47 37 141 645	324s 413s 772s 126s	0 37 0 276
		pms_in	601	183	515s	512	178s	330
	MSE19∪20	1000	270	422s	734	256s	481

0 2 1 38:16 Combining Clause Learning and Branch and Bound for MaxSAT SAT

  -based MaxSAT solvers use a CDCL SAT solver as a black box and do not interfere in the internal operations of the SAT solver when solving an instance, while MaxCDCL itself can be considered a SAT solver extended to handle soft conflicts. Both MaxCDCL and model-guided MaxSAT solvers have an upper bound UB-1 of the number of soft clauses that can be falsified. The difference lies in how to exploit this UB. Let f alseS denote the set of already falsified soft clauses. On the one hand, model-guided MaxSAT solvers call a SAT solver after encoding UB into CNF. If no hard clause is falsified, the SAT solver backtracks only after |f alseS| ≥ UB, because no clause encoding UB is falsified if |f alseS| < UB. On the other hand, MaxCDCL computes a lower bound LB of the number of soft clauses that will be falsified (but not yet falsified), and backtracks as soon as LB+|f alseS| ≥ UB. Thus, MaxCDCL is able to backtrack much earlier than model-guided MaxSAT solvers. MaxCDCL, core-guided or MHS-guided MaxSAT solvers all identify cores. However, a core-guided or MHS-guided MaxSAT solver only identifies global cores (i.e., the cores that do not depend on any partial assignment) in order to relax them, while MaxCDCL detects local cores by using UP under a partial assignment to derive a soft conflict for learning a clause and backtracking early. Note that identifying a global core is NP-hard, while detecting a local core by applying UP is polynomial.

The source code of MaxCDCL is available at https://home.mis.u-picardie.fr/~cli/EnglishPage. html

https://www.cs.toronto.edu/maxsat-lib/maxsat-instances/master-set/unweighted/

Funding This work has been partially funded by the French Agence Nationale de la Recherche, reference ANR-19-CHIA-0013-01, and the Spanish AEI project PID2019-111544GB-C2.

Acknowledgements This work has been partially supported by Archimedes Institute, Aix-Marseille University. We thank the anonymous reviewers for their comments and suggestions that helped to improve the manuscript.

: https://home.mis.u-picardie.fr/~cli/ EnglishPage.html


Charbel Rahhal
email: charbel.rahal@loria.fr

Hala Skaf-Molli

Pascal Molli
email: molli@loria.fr

Stéphane Weiss
email: weiss@loria.fr

Multi-synchronous Collaborative Semantic Wikis

Semantic wikis have opened an interesting way to mix Web 2.0 advantages with the Semantic Web approach. However, compared to other collaborative tools, wikis do not support all collaborative editing mode such as offline work or multi-synchronous editing. The lack of multi-synchronous supports in wikis is a problematic, especially, when working with semantic wikis. In these systems, it is often important to change multiple pages simultaneous in order to refactor the semantic wiki structure. In this paper, we present a new model of semantic wiki called Multi-Synchronous Semantic Wiki (MS2W). This model extends semantic wikis with multi-synchronous support that allows to create a P2P network of semantic wikis. Semantic wiki pages can be replicated on several semantic servers. The MS2W ensures CCI consistency on these pages relying on the Logoot algorithm.

Introduction

Wikis have demonstrated how it is possible to convert a community of strangers into a community of collaborators producing all together valuable contents. Semantic wikis [START_REF] Krötzsch | Semantic wikipedia[END_REF][START_REF] Schaffert | IkeWiki: A Semantic Wiki for Collaborative Knowledge Management[END_REF][START_REF] Skaf-Molli | Peer-to-peer semantic wikis[END_REF][START_REF] Buffa | Sweetwiki: A semantic wiki[END_REF] by introducing semantic annotations within wiki pages, have opened an interesting way to mix Web 2.0 advantages with the Semantic Web approach. However, compared to other collaborative tools, wikis do not support all collaborative editing mode such as offline work or multi-synchronous editing [START_REF] Dourish | The parting of the ways: Divergence, data management and collaborative work[END_REF][START_REF] Molli | State Treemap: an Awareness Widget for Multi-Synchronous Groupware[END_REF]. It is not possible to work with a wiki as it is possible to work with popular distributed version control systems (DVCS) [START_REF] Allen | ClearCase MultiSite: Supporting Geographically-Distributed Software Development[END_REF] such as Git and Mercurial. The lack of multi-synchronous support in wikis is a problematic, especially, when working with semantic wikis. In these systems, it is often important to change multiple pages simultaneous in order to refactor the semantic wiki structure. Without multi-synchronous support all incremental changes will be visible to both end users and semantic request engines. Therefore, they can observe inconsistent states of the wiki as in a database system without transactional support. We can say that existing wikis do not support transactional changes. Moreover, the lack of multi-synchronous support prevents users to work insulated [START_REF] Estublier | Impact of the research community on the field of software configuration management: summary of an impact project report[END_REF] and also prevents semantic wikis to support dataflow oriented workflow. One approach to solve this problem is to synchronize a network of semantic wikis using distributed version control systems. Unfortunately, DVCS do not support data types used in semantic wikis and do not ensure the CCI consistency model [START_REF] Sun | Achieving Convergence, Causality Preservation, and Intention Preservation in Real-Time Cooperative Editing Systems[END_REF] required for distributed collaborative environment. Another approach is to integrate the DVCS collaboration model into a semantic wikis and manage synchronization of wikis using a CCI preserving algorithm. This can be achieved by deploying a network of semantic wikis. Every node of the network replicates a subset of semantic wiki pages. Any node of the network can be connected to another using a publish/subscribe model. A node that publishes changes just push operations representing these changes in a feed. A node that subscribed to this feed can pull operations at any time and re-execute remote operations locally. In this paper, we present a new model of semantic wikis called Multi-Synchronous Semantic Wiki (MS2W). This model extends semantic wikis with multi-synchronous support that allows to create a P2P network of semantic wikis based on declarative collaborative community. Semantic wiki pages can be replicated on several semantic servers. The MS2W ensures CCI consistency on these pages relying on the Logoot algorithm [START_REF] Weiss | Logoot : a scalable optimistic replication algorithm for collaborative editing on p2p networks[END_REF]. In this paper, we define a MS2W ontology and algorithms. This ontology can be used to compute awareness metrics for working in multi-synchronous environment [START_REF] Molli | Divergence awareness for virtual team through the web[END_REF]. Finally, we demonstrate that combining these algorithms with the Logoot algorithm allow to preserve the CCI consistency model.

The paper is organized as follows. Section 2 presents background and related works. Section 3 gives an overview of the multi-synchronouns semantic wikis (MS2W) and shows scenarios of new collaboration mode in semantic wikis. Section 4 develops the data model, the algorithms for MS2W and presents the correction of our algorithms. Section 5 presents the implementation of the MS2W. The last section concludes the paper and points to some directions for future works.

Background and Related work

This section gives a brief overview of semantic wikis and shows their drawbacks. Then, it presents the definition and the principals of multi-synchronous collaboration. Finally, it presents the CCI consistency model.

Semantic Wikis

Semantic wikis such as Sematic MediaWiki [START_REF] Krötzsch | Semantic wikipedia[END_REF], IkeWiki [START_REF] Schaffert | IkeWiki: A Semantic Wiki for Collaborative Knowledge Management[END_REF], SweetWiki [START_REF] Buffa | Sweetwiki: A semantic wiki[END_REF] and SWooki [START_REF] Skaf-Molli | Peer-to-peer semantic wikis[END_REF] are a new generation of collaborative editing tools, they allow users to add semantic annotations in the wiki pages. These semantic annotations can then be used to find pertinent answers to complex queries. Semantic wikis can be viewed as an efficient way to better structure wikis by providing a means to navigate and answer questions or reason, based on annotations. Semantic wikis are an extension of wiki systems that preserve the same principles of wikis such as simplicity in creating and editing wikis pages. Semantic wikis embed semantic annotations in the wiki content by using Semantic Web technologies such as RDF and SPARQL. In semantic wikis, users collaborate not only for writing the wiki pages but also for writing semantic annotations. Traditionally, authoring semantics and creation ontologies has mainly been in the hand of "ontologists" and knowledge management experts. Semantic wikis allow mass collaboration for creating and emerging ontologies. Some existing semantic wikis allows the emergence of the ontology, MediaWiki(SMW) [START_REF] Krötzsch | Semantic wikipedia[END_REF] and SweetWiki [START_REF] Buffa | Sweetwiki: A semantic wiki[END_REF]. Others use the wikis as a collaborative ontologies editors. IkeWiki [START_REF] Schaffert | IkeWiki: A Semantic Wiki for Collaborative Knowledge Management[END_REF] aims to create an instance of existing ontologies, while OntoWiki [START_REF] Auer | Ontowiki -A tool for social, semantic collaboration[END_REF] aims the creation of ontology schema. In a semantic wiki, users add semantic annotations to wiki page text to represent relations and properties on this page. In SMW users choose their own vocabularies to type links. For instance, a link between the wiki pages "France" and "Paris" may be annotated by a user as "capital". These annotations express semantic relationships between wikis pages. Semantic annotations are usually written in a formal syntax so they are processed automatically by machines and they are exploited by semantic queries. In spite of their success, semantic wikis do not support a multi-synchronous work mode. Their current model provides only one copy of a semantic wiki page. The state of a semantic wiki page is always the current visible one on the server, intermediate inconsistent states are always visible. Consequently, transactional changes are not be supported neither the isolated work mode nor off-line editing mode. In previous work, we proposed SWooki [START_REF] Skaf-Molli | Peer-to-peer semantic wikis[END_REF] the first P2P semantic wiki. It combines the advantages of P2P wikis and semantic wikis. It is based on an optimistic replication algorithm that ensures the CCI consistency model. It supports the off-line work mode and transactional changes. Its main limitations are the total replication and the collaboration model. Every peer of the network hosts a replica of wiki pages and a replica of the semantic store. Users cannot choose the pages that they want to replicate neither the period of synchronization. Modifications are propagated on page saving. The collaborative community is implicit. Users cannot choose to whom propagate modifications. Changes propagation is under the control of system and not the users. All connected peers receive and integrate changes. A disconnected peer will receive the modifications of the others at reconnection thanks to the anti-entropy algorithm.

Multi-synchronouns Collaboration

Dourish wrote [START_REF] Dourish | The parting of the ways: Divergence, data management and collaborative work[END_REF], "The notion of multiple, parallel streams of activity, is a natural approach to supporting this familiar pattern of collaborative work. Working activities proceed in parallel (multiple streams of activity), during which time the participants are disconnected (divergence occurs); and periodically their individual efforts will be integrated (synchronization) in order to achieve a consistent state and progress the activity of the group".

Multi-synchronous applications are different from synchronous and asynchronous ones by managing multiple streams of activities instead of giving the illusion of one stream. In standard collaborative applications, when a modification is made by one user, it is immediately visible by others. However, in multi-synchronous applications, modifications made by one user is not visible by others. It becomes visible only when a user validates his modifications (commits his changes). A visible change does not imply immediate integration by other activities streams. Concurrent modifications will be integrated only when users will decide it. Allowing deferred validation of changes and divergence have several important advantages and impacts [START_REF] Molli | Divergence awareness for virtual team through the web[END_REF]: Parallelization of activities, privacy, invisibility of partial changes and experimental changes. Multi-synchronous authoring tools [START_REF] Dourish | The parting of the ways: Divergence, data management and collaborative work[END_REF][START_REF] Molli | State Treemap: an Awareness Widget for Multi-Synchronous Groupware[END_REF] allow simultaneous work in isolation and later integration of the contributions. They are characterized by their abilities to support divergence i.e parallel steam of activities on replicated data. SAMS [START_REF] Molli | Sams: Synchronous, asynchronous, multi-synchronous environments[END_REF] allows team members to work in synchronous, asynchronous or multi-synchronous mode while ensuring the coherence of the shared data. It uses an operational transformation algorithm to maintain the consistency of the shared data. Although it is independent of shared objects types, SAMS requires the design of transformation functions that depend on the type of the shared object. Design of transformation functions is a hard task and errors prone. Currently, there are no transformation functions designed for semantic wiki pages. Distributed Version Control Systems [START_REF] Allen | ClearCase MultiSite: Supporting Geographically-Distributed Software Development[END_REF] such Git manage files and directories. They are not used to track changes in semantic wiki pages. They ensure causal consistency, this implies that concurrent write operations can be seen in a different order on different machines. In this case, if two sites observe 2 write operations in different order then copies on both sites can diverge. DVCS systems are aware of this problem and delegate the problem to external merge algorithms for managing concurrent operations. However, as existing merge algorithms are not intrinsically deterministic, commutative and associative so convergence cannot be ensured in all cases.

CCI Consistency Model

A distributed collaborative system is composed of unbounded set of peers P . Objects modified by the system are replicated into a set of replicas R (with 0 < |R| ≤ |P |). Every replica has the same role and hosted on one peer. A peer can host replicas of different objects. Peers can enter and leave the network arbitrary. Every peer has a unique comparable identifier. The modifications applied on a replica are eventually delivered to all other replicas, then, they are applied locally. According to [START_REF] Sun | Achieving Convergence, Causality Preservation, and Intention Preservation in Real-Time Cooperative Editing Systems[END_REF], the system is correct if it ensures the CCI consistency model.

-Causality: This criterion ensures that all operations ordered by a precedence relation, in the sense of the Lamport's happened-before relation [START_REF] Lamport | Times, Clocks, and the Ordering of Events in a Distributed System[END_REF] will be executed in same order on every site.

-Convergence: The system converges if all replicas are identical when the system is idle (eventual consistency).

-Intention and Intention preservation: The intention of an operation is the effects observed on the state when the operation was generated. The effects of executing an operation at all sites are the same as the intention of the operation.

Many algorithms that verify the CCI model have been developed by the Operational Transformation community [START_REF] Sun | Achieving Convergence, Causality Preservation, and Intention Preservation in Real-Time Cooperative Editing Systems[END_REF] such as SOCT2, GOTO, COT etc.

But only few of them (MOT2 [START_REF] Cart | Asynchronous reconciliation based on operational transformation for p2p collaborative environments[END_REF]) support the join and leave constraint of P2P network. However, MOT2 algorithm suffers from a high communication complexity. WOOT [START_REF] Oster | Data Consistency for P2P Collaborative Editing[END_REF] is the first synchronization algorithm that ensures the CCI consistency and respects the P2P constraints. WOOT is used in Wooki [START_REF] Weiss | Wooki: a p2p wiki-based collaborative writing tool[END_REF] a peer-to-peer wiki and an modified version of WOOT that takes in consideration semantic data is implemented in SWooki [START_REF] Skaf-Molli | Peer-to-peer semantic wikis[END_REF]. Recently, an optimized version of WOOT called Logoot is published in [START_REF] Weiss | Logoot : a scalable optimistic replication algorithm for collaborative editing on p2p networks[END_REF], it ensures convergence and preserves the intentions, if the causality is preserved.

Multi-synchronous Semantic Wiki Approach

Multi-synchronous semantic wikis allow users to build their own cooperation networks. The construction of the collaborative community is declarative, in the sense, every user declares explicitly with whom he would like to cooperate. Every user can have a multi-synchronous semantic wiki server installed on her machine. She can create and edit her own semantic wiki pages as in a normal semantic wiki system. Later, she can decide to share or not these semantic wiki pages and decide with whom to share.

Multi-synchronous Collaboration Model

The replication of data and the communication between servers is made through channels (feeds). The channel usage is restricted to few servers with simple security mechanisms that requires no login and complex access control. Capabilities fit perfectly these requirements [START_REF] Levy | Capability-Based Computer Systems[END_REF]. The key point is that channels are read-only for consumers and can be hosted on hardware of users. When a semantic wiki page is updated on a multi-synchronous semantic wiki server, it generates a corresponding operation. This operation is processed in four steps: (1) It is executed immediately against page, (2) it is published to the corresponding channels, (3) it is pulled by the authorized servers, and (4) it is integrated to their local replica of the page. If needed, the integration process merges this modification with concurrent ones, generated either locally or received from a remote server.

The system is correct if it ensures the CCI (Causality, Convergence and Intention Preservation) consistency model. Multi-synchronous semantic wikis use the Logoot synchronization algorithm [START_REF] Weiss | Logoot : a scalable optimistic replication algorithm for collaborative editing on p2p networks[END_REF] to integrate modifications. Logoot ensures the CCI consistency model. More precisely, Logoot ensures convergence and preserves the intentions of operations if the causality of the operations is preserved.

Collaboration Scenarios

This section presents two scenarios of collaboration in multi-synchronouns semantic wikis. We suppose several professors collaborate together through a semantic wiki to prepare lectures, exercises and exams. Later, they want to make lectures available for students and they want to integrate relevant feedbacks from students. Scenario 1: Collaboration among professors For simplicity, we suppose there are two professors prof 1 and prof 2 (see figure 1). Every professor has her own multisynchronous semantic wiki, site 1 for prof 1 and site 2 for prof 2 , respectively. 2. prof 1 wants to publish her modifications on lesson 1 to prof 2 . Therefore, she creates a feed url 1 that contains change set. Finally, she communicates the address of the feed to prof 2 . 3. prof 2 subscribes to this channel and creates a feed url 2 to pull modifications.

The result is a local semantic wiki page lesson 1 that has the same content as lesson 1 of prof 1 . 4. prof 2 edits his local copy of the lesson 1 page. lesson 1 has now five lines: 5. In her turn, prof 2 shares his modifications on lesson 1 with prof 1 . He creates a feed and publishes his modifications. prof 1 subscribes to the feed and pulls the modifications published by prof 2 and finally integrates these modifications on her local copy of lesson 1 . The integration process merges the remote modifications with concurrent ones, if any, generated locally by prof 1 . The integration process has to ensure the convergence of all copies on lesson 1 if all generated operations on site 1 and site 2 are integrated on both sites.

The advantages of this collaboration model are, on the one hand, there is no need for centralized server to cooperate. On the other hand, every professor works on her or his own copy in isolation, publishes and pulls changes whenever she wants, i.e. the changes propagation is under the control of the user. This collaboration process is not supported in classical semantic wikis. The table 1 represents a part of the scenario. wants to make lesson 1 available for her students while she continues to make corrections and minor modifications on lesson 1 . In order to provide her students with the courses, prof 1 publishes them on a public site pubSite that can be either her proper public wiki site or the site of the university. pubSite is accessible by the students for read only to maintain the courses consistency. However, prof 1 manages to integrate relevant feedbacks from students provided by the students sites.

Professor can make continuous improvement of the lessons and can make continuous integration of the modifications and make only consistent modifications visible. Without multi-synchronous support all incremental changes will be visible to both end users and to semantic request engines. Every participant professor and student want to control the visibility of their modifications and want to control the integration of others' modifications.

Multi-synchronous Semantic Wiki System

This section presents the data model and the algorithms for multi-synchronous Semantic Wiki systems (M2SW). The data model is defined an ontology. Therefore, it is possible to querying and reasoning on the model itself and make future extension. For instance, it is possible to make queries like: (1)"list all unpublished changes", ( 2) "list all published changes on a given channel", (3) "list unpublished change set of a given semantic wiki page", ( 4) "list all pulled change sets", etc.

MS2W Ontology

The M2SW ontology is defined as an extension of existing ontologies of semantic wikis [START_REF] Buffa | Sweetwiki: A semantic wiki[END_REF]. In this section, we present the M2SW ontology and detail only its new vocabulary and their properties.

-WikiSite : this concept corresponds to a semantic wiki server. A site has the following properties: • siteID : this attribute contains the U RL of the site.

• logicalClock : this attribute has a numeric value. Every semantic wiki server maintains a logical clock, this clock is used to identify patches and operations in an unique way in the whole network. • hasP ush, hasP ull and hasP age : the range of these properties are respectively a push feed, a pull feed and a semantic wiki page. A wiki site has several push feeds, pull feeds and several pages . -SemanticWikiPage: this concept corresponds to a normal semantic wiki page. It has the following properties:

• pageID : this attribute contains the U RL of the page.

• hasContent the range of this property is a String, it contains text and the semantic data embedded in the semantic wiki page. • head : this property points to the last patch applied to the page.

-Operation : this concept represents a change in a line of a wiki page. In our model, there are two editing operations : insert and delete. An update is considered as a delete of old value followed by an insert of a new value. An operation has the following properties:

• operationID: this attribute contains the unique identifier of the operation. operationID is calculated by: operationID = concat(Site.siteID, Site.logicalClock + +), the concat function concatenates two strings. • opT ype: this attribute contains the type of the operation, it can be either an insert or a delete.

• positionID: denotes the position of the line in the wiki page. This identifier is calculated by the Logoot algorithm [START_REF] Weiss | Logoot : a scalable optimistic replication algorithm for collaborative editing on p2p networks[END_REF]. • lineContent: is a string representing text and the semantic data embedded in the line.

-Patch : a patch is a set of operations. A patch is calculated during the save of the modified semantic wiki page using the Logoot algorithm. A patch has the following properties:

• patchID: is a unique identifier of the patch. Its value is calculated by : patchID = concat(Site.siteID, Site.logicalClock + +) • onP age: the range of this property is the page where the patch was applied. • hasOperation: this property points to the operations generated during the save of the page. • previous: points to the precedent patch.

-ChangeSet : a change set contains a set of patches. This concept is important in order to support transactional changes. It allows to regroup patches generated on multiple semantic wiki pages. Therefore, it is possible to push modifications on multiple pages. ChangeSet has the following properties:

• changSetID: is a unique identifier of a change set. Its value is calculated as : changeSetID = concat(Site.siteID,Site.logicalClock + +) • hasP atch property points to the patches generated since the last push.

• previousChangeSet: points to the precedent change set.

• inP ushF eed: the range of this property is P ushF eed. This property indicates the P ushF eed that publishes a ChangeSet. • inP ullF eed: the range of this property is P ullF eed . This property indicates the P ullF eed that pulls a ChangeSet.

-PushFeed : this concept is used to publish changes of a W ikiSite. It is a special semantic wiki page. It inherits the properties of the SemanticWikiPage concept and defines its own properties:

• hasP ushHead : this property points to the last published changeSet.

• hasSemanticQuery: this property contains a semantic query. This query determines the content of the push feed. For instance, the query can be "find all Lessons", this will return all the pages in the class (category)

Lessons. To answer hasSemanticQuery, reasoning and querying capabilities of semantic wikis are used.

-Pull Feed : this concept is used to pull changes from a remote W ikiSite.

A pull feed is related to one push feed. In the sense that it is impossible to pull unpublished data. A pull feed is also a special semantic wiki page. It inherits the properties of the Semantic Wiki Page concepts and defines it own properties:

• hasP ullHead: this property points to the last pulled change set pulled.

• relatedP ushF eed: this property relates a pull feed to the U RL of its associated push feed.

We can extend and build on M S2W ontology. The M S2W ontology is maintained by the M S2W developers. It is defined in OWL DL allowing to querying and reasoning on the patches, ChangeSet, PushFeed, etc. SPARQL can be used to query the MS2W data. For instance, it is possible to list all published patches on a push feed: P ublished ≡ ∃(hasP atch -1 ).∃(inP ushF eed -1 ).P ushF eed

Algorithms

As any semantic wiki server, a multi-synchronous semantic wiki server defines a Save operation which describes what happens when a semantic wiki page is saved. In addition, we define special operations : CreatePushFeed, Push, Cre-atePullFeed, Pull and Integrate for the multi-synchronous semantic wiki. We use the Logoot algorithm [START_REF] Weiss | Logoot : a scalable optimistic replication algorithm for collaborative editing on p2p networks[END_REF] for the generation and the integration of the insert and delete operations. In the following, detail these operations for a semantic wiki server called site.

Save Operation During the saving a wiki page, the Logoot algorithm computes the difference between the saved and the previous version of the page and generates a patch. A patch is a set of delete and insert operations on the page (Op = (opT ype, operationID, positionID, lineContent)). Logoot calculates the positionID, lineContent and the opT ype of the operation. These operations are integrated locally and then eventually published on a push feed. CreatePushFeed Operation The communication between multi-synchronouns semantic wiki servers is made through feeds. The CreatePushFeed operation creates of a push feed. A push feed is a special semantic wiki page that contains a query that specifies the pushed data. It is used to publish changes of a wiki server. Authorized sites can access the published data. CreatePushFeed operation calls the Push operation. semantic wiki pages. They stored in a special namespace to prevent user modification. The Logoot algorithm has been implemented in PHP and integrated in Mediawiki relying on the hook mechanism. The push, pull, createPushFeed and createPullFeed operations are available in special administration pages of Medi-aWiki as shown in figure 7. This extension is designed to respect the simplicity of the wikis while supporting the MS2W model and the result is an easy way to construct a P2P network of semantic wikis based on Semantic MediaWiki. In this paper, we propose a new model of semantic wikis called Multi-Synchronous Semantic Wiki (MS2W). MS2W extends a semantic wiki with multi-synchronous capabilities. Multi-synchronous semantic wikis allow users to build their own cooperation networks. The construction of the collaborative community is declarative. Every user declares explicitly with whom he would like to cooperate. The replication of the wiki pages on semantic wikis servers and the synchronization periods are variant and under the control of the users. The MS2W model enhances the existing semantic wikis by supporting transactional changes and the off-line work mode. Hence, multiple dataflow oriented workflows can be supported. In addition, the model takes natural advantages of a P2P network, i.e. faults-tolerance, better scalability, infrastructure cost sharing and better performance. In the paper, we develop an ontology for MS2W. Each ontological element in this wiki is exploitable, consequently advanced reasoning and querying capabilities are provided. We develop also a set of algorithms for the creation and the replication of semantic wiki pages and for the propagation and the synchronization of changes between the peers. The MS2W algorithm ensures the CCI consistency on the pages. We are currently implementing the MS2W model as an extension of Semantic MediaWiki. As for future works, we want to support the MS2W with two crucial features: (1) an undo mechanism to facilitate the undo of undesired merge results, (2) an advanced mechanism for divergence metrics based on querying the semantic annotations.

Fig. 1 .

 1 Fig. 1. multi-synchronous semantic wikis scenario

1 .

 1 prof 1 edits three semantic wiki pages lesson 1 , exercises 1 and exam 1 on her site site 1 . For instance, the page lesson 1 edited by prof 1 has three lines: Introduction: In "multi-synchronous" work, parties work independently in parallel. [Category::Lesson] [forYear:2009]

  Introduction:In "multi-synchronous" work mode, parties work independently in parallel.[Category::Lesson] [forYear:2009]. This mode is based on divergence and synchronization phases.

Fig. 2 .

 2 Fig. 2. Multi-synchronous ontology

Fig. 7 .

 7 Fig. 7. MS2W Administration page

Table 1 .

 1 Multi-synchronous collaboration scenarioScenario 2: Collaboration among professors and students In this scenario, prof 1

	Site1	Site2
	Edit(lesson1)
	Edit(exercises1)
	Edit(exam1)
	CreatePushFeed(f1,q1)
		CreatePullFeed(f1, f2)
	Edit( lesson1)	Edit( lesson1)
	Push(f1)
		CreatePushFeed(f3,q2)

On CreatePushFeed(name:String,request:String): PushFeed(name) hasSemanticQuery(name,request) hasPush(site,name) call Push(name)

Push Operation This operation creates a change set corresponding to the pages returned by the semantic query and adds it to the push feed. Firstly, the semantic query is executed, then the patches of the pages returned by the query are extracted. These patches are added to the change set if they have not been published on this push feed yet. CreatePullFeed Operation As the replication of data and the communication between multi-synchronouns semantic wiki servers are made through feeds, pull feeds are created to pull changes from push feeds on remote peers to the local peer (cf figure 3). A pull feed is related to a push feed. In the sense that it is impossible to pull unpublished data. get Function This function allows to retreive a ChangeSet (cf figure 4).

Integration operation

The integration of a change set is processed as follows (cf figure 6). First all the patches of the change set are extracted. Every operation in the patch is integrated in the corresponding semantic wiki page thanks to the Logoot algorithm.

Correction model

Theorem 1. Our algorithms ensure the causality.

proof A site always respects the causality of its own operations since it generates these operations alone, so these operations placed in the push feed are causal. In the following, we take an hypothesis that a site S pulls from N sites that ensure the causality and we want to prove that the site itself ensures the causality. We will prove that the site S cannot violate the causality through the contradiction proof. Let us consider that the site S violates the causality, i.e. in the content of its push feed there is an operation op 2 that depends causally (Lamport dependence) on an operation op 1 and op 2 is placed before op 1 in that feed. The operations in a push feed has two different sources either they are local generated by the site itself or the site had received them from other sites. Let us study both cases (1) local operations: the local operations always respect the causality, so a site is not going to violate the causality. (2) remote operations: In order to get the operation op 2 placed at the position N in the push feed of site S, S must pull, i.e. copy all the operations that precedes op 2 . Getting op 2 without having op 1 means that op 1 was not among the N -1 operations that precedes op 2 in the push feed which violates the hypothesis that the site S pulls only from N sites that respect the causality. Consequently, it is not possible to find op 2 before op 1 . Therefore, a site always respects the causality alone. If this site pulls from N sites that ensure the causality, it ensures the causality itself. In recurrence, all site ensure the causality for any N , where N is an integer. Hence, our algorithm ensures the causality for all the sites in the network. Theorem 2. Our algorithms ensure the CCI model (Causality, Convergence, Intention).

proof Our algorithm is based on Logoot algorithm for the generation and the integration of the operations. It is proved in [START_REF] Weiss | Logoot : a scalable optimistic replication algorithm for collaborative editing on p2p networks[END_REF], that the Logoot algorithm ensures the convergence and preserves the intentions, if the causality is preserved. Since our algorithms ensure the causality (theorem 1), hence it ensures also the convergence and preserves the intentions.

Implementation

We are currently implementing the MS2W model as an extension of Semantic MediaWiki [START_REF] Krötzsch | Semantic wikipedia[END_REF]. Feeds, ChangeSets and Patches are represented as special