Gilles Audemard
email: audemard@cril.fr

Benoît Hoessen
email: hoessen@cril.fr

Saïd Jabbour
email: jabbour@cril.fr

Jean-Marie Lagniez
email: jean-marie.lagniez@jku.at

Cédric Piette
email: piette@cril.fr

Revisiting Clause Exchange in Parallel SAT Solving

Managing learnt clause database is known to be a tricky task in SAT solvers. In the portfolio framework, the collaboration between threads through learnt clause exchange makes this problem even more difficult to tackle. Several techniques have been proposed in the last few years, but practical results are still in favor of very limited collaboration, or even no collaboration at all. This is mainly due to the difficulty that each thread has to manage a large amount of learnt clauses generated by the other workers. In this paper, we propose new efficient techniques for clause exchanges within a parallel SAT solver. In contrast to most of the current clause exchange methods, our approach relies on both export and import policies, and makes use of recent techniques that proves very effective in the sequential case. Extensive experimentations show the practical interest of the proposed ideas.

Introduction

The practical resolution of the SAT problem has received major attention these two last decades. Particularly, due to the wide availability of cheap multicore architectures, the focus is now on the development of efficient parallel engines, able to solve large realworld problems. Several of them have been recently proposed, e.g. ManySat [START_REF] Hamadi | Manysat: a parallel SAT solver[END_REF], SArTagnan [START_REF] Kottler | SArTagnan -a parallel portfolio SAT solver with lockless physical clause sharing[END_REF], Plingeling [START_REF] Biere | lingeling[END_REF], ppfolio [START_REF] Roussel | [END_REF], part-tree-learn [START_REF] Eero | Grid-based SAT solving with iterative partitioning and clause learning[END_REF].

Portfolio schema is a possible approach to tackle parallelism. One idea of portfolio algorithms is the collaboration between the different workers. In the SAT case, their joint effort is mainly achieved through the exchange of learnt clauses. Unfortunately, it is very hard to predict whether a clause generated by a working thread will be useful for the others, or not. To deal with this problem, ManySAT proposes a dynamic clause sharing policy which uses pairwise size limits to control the exchange between threads [START_REF] Hamadi | Control-based clause sharing in parallel SAT solving[END_REF]. However, most of implementations (Plingeling [START_REF] Biere | lingeling[END_REF], SArTagnan [START_REF] Kottler | SArTagnan -a parallel portfolio SAT solver with lockless physical clause sharing[END_REF], etc.) only share unit clauses with the other threads. Moreover, in the last SAT competition, a new portfolio called ppfolio obtained very good results; ppfolio is actually a simple script that runs different state-of-art sequential solvers in an independent way. Accordingly, no collaboration is achieved within this solver, and yet it proves very efficient during this competition. This shows that the current clause exchange techniques are not mature and may be improved.

The problem of predicting the usefulness of a given learnt clause is also known in the sequential case; recently, a new measure called psm [START_REF] Audemard | On freezeing and reactivating learnt clauses[END_REF] has been proposed to dynamically manage learnt clauses. Roughly, it consists in comparing the current (partial) interpretation to the set of literals of each learnt clause. The main idea is the following: if the set-theoretical intersection of the current interpretation and the clause is large, then the clause is unlikely useful in the current part of the search space. On the contrary, if this intersection is small, then the clause has a lot of chance to be useful for unit-propagation, reducing the search space. This measure has been used in a new strategy to manage the learnt clauses database which enables to freeze a clause, namely to remove it from the set of learnt clauses on a temporary basis, when it is considered "useless". Periodically all clauses are reevaluated in other to be frozen or activated. This technique proves very efficient in an empirical point of view, and succeeds to select relevant learnt clauses.

In this paper, we extend the results of [START_REF] Audemard | On freezeing and reactivating learnt clauses[END_REF] to the portfolio framework, proposing different efficient heuristical policies for exporting, importing and selecting relevant clauses for the different threads of a portfolio. This paper is structured as follows: in the next Section, we present the background knowledge about parallel SAT solving and learnt clause management. In the Section 3, we present some preliminaries about the behavior of a portfolio solver. Next, in Section 4, our case study solver called PeneLoPe is presented and it is compared to the best parallel SAT solvers in Section 5. Finally, we conclude with some perspectives.

Technical Background

First of all, we assume that the reader is familiar with Satisfiability notions (variables, literal, clause, unit clause, interpretations, CNF formula). Note that clauses and interpretations will be equally interpreted as set of literals. We just want to recall the global schema of CDCL (Conflict-Driven, Clause Learning) solvers: a typical branch of a CDCL solver can be seen as a sequence of decisions followed by propagations, repeated until a conflict is reached. Each decision literal, chosen by some heuristic, usually activity-based ones, is assigned at its own level, shared with all propagated literals assigned at the same level. Each time a conflict is reached, a nogood is extracted using a particular method, usually the First UIP (Unique Implication Point) one [START_REF] Marques-Silva | GRASP -A New Search Algorithm for Satisfiability[END_REF][START_REF] Zhang | Efficient conflict driven learning in boolean satisfiability solver[END_REF]. The learnt clause is then added to the learnt clause database and a backjumping level is computed from it. The interested reader can refer to [START_REF] Darwiche | Complete Algorithms[END_REF] for more details. In the rest of the section, we give background about important notions for the paper understanding.

Control of the learnt clauses database

The size of the learnt clauses database is clearly crucial to the solver performance. Indeed, keeping too many learnt clauses slows down the unit propagation process, while deleting too many of them breaks the overall learning benefit. To avoid such drawbacks, solvers periodically remove some clauses considered to be useless. Consequently, identifying good learnt clauses -relevant to the proof derivation -is clearly an important challenge. The first proposed quality measure follows the success of the activity-based VSIDS heuristic. More precisely, a learnt clause is considered relevant to the proof, if it is often involved in recent conflicts i.e. frequently used to derive asserting clauses. Clearly, this deletion strategy supposes that a useful clause in the past could be useful in the future. In [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF], another measure called lbd is used to estimate the quality of a learnt clause (we denote lbd(c) the lbd value of a clause c). This new measure is based on the number of different decision levels appearing in a learnt clause and is computed when the clause is generated. Extensive experiments demonstrates that clauses with small lbd values are used more often than those with higher lbd ones. Note also that lbd of clauses can be recomputed when they are used for unit propagations, and updated if the it becomes smaller. This update process is important to get many good clauses. However, these both measures are obviously heuristical ones and solvers are not safe from regularly eliminating relevant learnt clauses.

Parallel SAT solving

Two approaches are commonly explored to parallelize SAT solvers. The first one is mainly a divide-and-conquer idea, which divides the search space into subspaces, successively allocated to SAT workers. Each time a worker finish its job (whereas the other ones are still doing their task), a load balancing strategy is invoked, and dynamically transfers subspaces to this idle worker [START_REF] Chrabakh | GrADSAT: A parallel SAT solver for the grid[END_REF][START_REF] Chu | Pminisat: a parallelization of minisat 2.0[END_REF]. A closely related approach is the iterative partitioning one [START_REF] Eero | Grid-based SAT solving with iterative partitioning and clause learning[END_REF]. Note that some of these approaches are able to share clauses [START_REF] Schubert | Pamiraxt: Parallel SAT solving with threads and message passing[END_REF][START_REF] Eero | Grid-based SAT solving with iterative partitioning and clause learning[END_REF] between workers. On the other hand, the parallel portfolio strategy exploits the complementarity between different sequential CDCL strategies to let them compete and cooperate on the same formula [START_REF] Hamadi | Manysat: a parallel SAT solver[END_REF][START_REF] Biere | lingeling[END_REF][START_REF] Kottler | SArTagnan -a parallel portfolio SAT solver with lockless physical clause sharing[END_REF]. Since each worker deals with the whole formula, there is no need to introduce load balancing overheads, and cooperation is only achieved through the exchange of learnt clauses. With this approach, the crafting of the strategies is important, especially with a small number of workers. In general, the objective is to cover the space of good search strategies in the best possible way. Such strategies are efficient on multicore architectures.

As we said above, the size of the learnt clause database is crucial for sequential solvers. Then, for a parallel portfolio SAT solver, it is not desirable to share all learnt clauses between all threads. To deal with this problem, one has to select carefully the clauses that a thread wants to share with the others. A natural solution is to take into account the size of learnt clauses and share only the smallest ones (size less than 8 for example [START_REF] Hamadi | Manysat: a parallel SAT solver[END_REF]). Based on the observation that small clauses appears less and less during the search, authors of ManySAT propose a dynamic clause sharing policy which uses pairwise size limits to control the exchange between threads [START_REF] Hamadi | Control-based clause sharing in parallel SAT solving[END_REF].

However, it is surprising that Plingeling, one of the winner of the SAT'11 competition shares between threads only unit clauses. Furthermore, ppfolio which have obtained good results in that competition runs different state-of-art sequential solvers in an independent way without any sharing. This last observations show that current clause exchange techniques are not mature and may be improved. This is one of the goal of this paper.

Parallelism, Collaboration and Clause Exchange: a Premilinary Experimentation

To illustrate the current behavior of portfolio solvers with respect to clause exchanges, we first have conducted preliminaries experiments on a state-of-the-art solver. For a sequential solver, a "good" learnt clause is a clause that is used during the unit propagation process and the conflict analysis. For portfolio solvers, one can quite safely state the same idea: a "good" shared clause is a clause that helps at least one other thread reducing its search space, namely propagating. Accordingly, we wanted to know how useful are the clauses shared in a portfoliobased solver. To this end, we ran some experiments3 using a state-of-the-art portfoliobased SAT solver. We choose the solver ManySAT 2.0 (based on Minisat 2.2), because in this solver, the only difference between the working threads are caused by the first decision variables which are selected randomly. Except this initial interpretation, each DPLL worker exhibits the exact same behavior (in terms of restart strategy, branching variable heuristics, etc.), which allows us to make a fair comparison about clause exchange without any side effect. Hence, it represents a good framework to deal with parallel SAT solvers and clauses sharing. By default all clauses of size less than 8 are shared. Moreover, ManySAT provides a deterministic mode [START_REF] Hamadi | Deterministic parallel DPLL[END_REF]. Let us emphasize that we have activated this option to make the obtained results fully reproducible and we report the detailled results online 4 .

Let SC be the set of shared clauses, namely the set-theoretical union of each clause exported by a given thread to all the other ones. In this experiment, for each thread, we have considered two particular kinds of shared clauses. First, the shared clauses that are actually used (at least once) by a working thread to propagate. We denote this set used(SC). Second, we have also focused on the set of shared clauses that are deleted without having been from any help during the search. This set is denoted unused(SC). Clearly, SC\(used(SC) ∪ unused(SC)) represents the set of clauses that have neither been used nor been deleted, yet.

Figure 1 synthetizes the results obtained during this first experiment. The results are reported in the following way: each point of Figure 1 is associated with an instance, and the x-axys corresponds to the rate #used(SC)/#SC, whereas the y-axys corresponds to the rate #unused(SC)/#SC, and we report the average rate over the different threads. Figure 1(a) gives the results for ManySAT. First of all, we can remark that the rate of useful shared clauses differs greatly over different instances. We can also note, that in a lot of cases, ManySAT keeps shared clauses during the entire search (dots near the x-axys). This is due to the non-aggressive cleaning strategy of Minisat where in many instances no cleaning are performed. Threads can keep useless clauses a long time and have to support an over cost without any benefit. We have conducted the same experiment with a much more agressive cleaning strategy. We have choosed the one presented in [START_REF] Audemard | On freezeing and reactivating learnt clauses[END_REF] (see Section 4) and we report the result in Figure 1(b). Here, in many cases, shared clauses are deleted without any usage and the percentage of shared clauses that are used at least one time decreases with respect to the basic version of ManySAT. These results can be explained quite easily. If only few cleanings are done, the threads have to manage a lot of useful and useless shared clauses. In one hand, it owns a lot of information about the problem to solve, and propagates many units clauses. On the other hand, such a solver has to maintain a large number of clauses uselessly, which greatly slows down its exploration.

Conversely, when many cleanings are achieved, another problem occurs. Indeed, if a given clause is not used in conflict analysis and/or unit propagation very often, it has then a lot of chances to be quickly removed. Therefore, threads using an agressive strategy spend a lot of time importing clauses that are never used. We can also notice that only using the lbd measure for clause usefulness seems not efficient. Indeed, shared clauses are here small clauses, so they have small lbd values. Even if we can try to tune the cleaning strategy to obtain a stronger solver, we think that the classical strategy used to manage learnt clauses is not appropriate in the case of clauses sharing and multicore architectures. We propose a new scheme in the next section.

Selecting, Sharing and Activating Good Clauses

Managing learnt clauses is known to be difficult in the sequential case. Furthermore, dealing with imported clauses from other threads leads to additional problems:

-Imported clauses can be subsumed by clauses already present in the database. Since subsumption computation is time consuming, it is necessary to give the possibility to remove periodically learnt clauses. -Imported clauses may be useless during a long time, and suddenly become useful.

-Each thread has to manage many more clauses.

-Characterizing good imported clauses is a real challenge. For all of these reasons, we propose to use the dynamic management policy of learnt clauses proposed in [START_REF] Audemard | On freezeing and reactivating learnt clauses[END_REF] inside each thread. This recent technique enables to activate or freeze some learnt clauses, imported or locally generated. The advantage is twofold. The overhead caused by imported clauses is greatly reduced since clauses can be frozen. Nevertheless, clauses estimated useful in the next future of the search are activated. Let us present more precisely this method in the next Section.

Freezing clauses

The strategy proposed in [START_REF] Audemard | On freezeing and reactivating learnt clauses[END_REF] differs from the other ones proposed in the past (see Section 2). Indeed, it is based on a dynamic freezing and activation principle of learnt clauses. At a given search state, it activates the most promising learnt clauses while freezing irrelevant ones. In this way, learned clauses can be discarded from the current step, but may be activated again in future steps of the search process. This strategy cannot be used with the other known measures such as activity or lbd-based ones. Indeed, the activity (VSIDS-based) measure is dynamic but can only be used to update the activity of learnt clauses currently in the database, while the lbd value of a given learnt clause is either static (and does not change during search) or dynamic but, in this case, the same problem as VSIDS-based one occurs. Then, this strategy is associated with another measure, defined in the following, for identifying good learnt clauses [START_REF] Audemard | On freezeing and reactivating learnt clauses[END_REF].

Let Σ be a CNF formula, c be a clause learnt by the solver, and ω the current interpretation saved from the polarity choice of decision variables [START_REF] Pipatsrisawat | A lightweight component caching scheme for satisfiability solvers[END_REF]. The psm value of the clause c w.r.t. ω, denoted psm ω (c), is equal to:

psm ω (c) = |ω ∩ c|
psm is a highly dynamic measure, since it is mainly based on the current interpretation. It aims at selecting relevant context (i.e. learnt clauses) with respect to the search in progress. To this end, the clauses that exhibit a low psm are considered relevant. Indeed, the lower is a psm value, the more likely the related clause is about to unit-propagate some literal, or to be falsified. On the opposite, a clause with a large psm value has a lot of chance to be satisfied by many literals, making it irrelevant for the search in progress.

Thus, only clauses that exhibit a low psm are selected and currently used by the solver, the other clauses being frozen. When a clause is frozen, it is removed from the list of the watched literals of the solver, in order to avoid the computational overhead of maintaining the data structure of the solver for this useless clause. Nevertheless, a frozen clause is not erased but it is kept in memory, since this clause may be useful in the next future of the search. As the current interpretation evolves, the set of learnt clauses actually used by the solver evolves, too. In this respect, the psm value is computed periodically, and sets of clauses are frozen or unfrozen with respect to their freshly computed new value.

Let P k be a sequence where P 0 = 500 and P i+1 = P i + 500 + 100 × i. A function "updateDB " is called each time the number of conflict reaches P i conflicts (where i ∈ [0..∞]). This function computes new psm values for every learnt clauses (frozen or activated). A clause that has a psm value less than a given limit l is activated in the next part of the search. If its psm does not hold this condition, then it is frozen. Moreover, a clause that is not activated after k (equal to 7 by default) time steps is deleted. Similarly, a clause remaining active more than k steps without participating to the search is also permanently deleted.

Given the psm and lbd measures, we now define different policies for clause exchange. In a typical CDCL procedure, a nogood clause is learnt after each conflict. It appears that all clauses cannot be shared, especially because some of them are not useful in a long term. So, when collaboration is achieved, this is limited through some criterion. To the best of our knowledge, in all current portfolio solvers, this criterion is only based on the information from the sender of the clause, the receiver having to accept any clause judged locally relevant by another worker.

We present in the next Section a technique where both the sender and the receiver of a clause havea strategy. Obviously, any sender (export strategy) tries to find in its own learnt clause database the most relevant information to help the other workers. However, the receiver (import strategy) here does not accept the shared clauses in a blind way. We have called our case study solver PeneLoPe5 (Parallel Lbd Psm solver).

Importing clause policy When a clause is imported, we can consider different cases, depending on the moment the clause is attached for participating to the search.

no-freeze: each imported clause is actually stored with the current learnt database of the thread, and will be evaluated (and possibly frozen) during the next call to updateDB .

freeze-all: each imported clause is frozen by default, and is only used later by the solver if it is evaluated relevant w.r.t. unfreezing conditions. freeze: each imported clause is evaluated as it would have been if locally generated.

If the clause is considered relevant, it is added to the learnt clauses, otherwise it is frozen.

Exporting clause policy Since PeneLoPe can freeze clauses, each thread can import more clauses than it would with a classical management of clauses, where all of them are attached. Then, we propose different strategies, more or less restrictive, to select which clauses have to be shared:

unlimited: any generated clause is exported towards the different threads.

size limit: only clauses whose size is less than a given value (8 in our experiments) are exported [START_REF] Hamadi | Control-based clause sharing in parallel SAT solving[END_REF]. 1. Comparison between import, export & restart strategies using deterministic mode lbd limit: a given clause c is exported to other threads if its lbd value lbd(c) is less than a given limit value d (8 by default). Let us also note that the lbd value can vary over time, since it is computed with respect to the current interpretation. Therefore, as soon as lbd(c) is less than d, the clause is exported.

Restarts policy Beside exchange policies, we define two restart strategies.

-Luby: Let l i be the i th term of the Luby serie [START_REF] Luby | Optimal speedup of Las Vegas algorithms[END_REF]. The i th restart is achieved after l i × α conflicts (α is set to 100 by default).

-LBD [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF]: Let LBD g be the average value of the LBD of each learnt clause since the beginning. Let LBD 100 be the same value computed only for the last 100 generated learnt clause. With this policy, a restart is achieved as soon as LBD 100 × α > LBD g (α is set to 0.7 by default). In addition, the VSIDS score of variables that are unit-propagated thank for a learnt clause whose lbd is equal to 2 are increased, as detailled in [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF].

We have conducted experiments to compare these different import/export/restart strategies. We ran these different versions and Table 1 presents a sample of the obtained results This table report for each strategy the number of SAT instances solved (#SAT), together with the number of UNSAT instances solved (#UNSAT) and total (#SAT + #UNSAT).

Let us take a first look at the export strategy. Unsurprisingly, the "unlimited" policy obtained the worst results. Indeed, none of these versions have been able to solve more than 190 instances, regardless all other policies (export, restart). Here, every generated clause is exported, and we reach the maximum level of communication. As expected, with the multiplicity of the workers, the solvers are soon overwhelmed by clauses and their performances drop. This was the reason why a size-based limit was introduced with the idea that the smallest clauses produce the best syntactic filtering, and therefore are preferable. Indeed, in Table 1, it appears clearly that "size limit" (clauses containing less than 8 literals) policy outperforms the "unlimited" one. This simple limit shows its usefulness, but a main drawback is that it has been shown [START_REF] Beame | Towards understanding and harnessing the potential of clause learning[END_REF] that longer clauses may greatly reduce the size of the proof.

Using the lbd value lbd(c) of a clause c can improve the situation as lbd(c) ≤ size(c). Hence, if the same value v is used for both the size and the lbd limits, more clauses are exported with the lbd policy. So, specifying a limit on the lbd allows us to import larger clauses if those ones are heuristically considered as promising. This could represent a problem for a parallel solver without the ability to freeze some clauses. Nevertheless, as PeneLoPe contains such mechanism, the impact is greatly reduced. From an empirical point of view, Table 1 shows that the "lbd limit" obtains the best results among all exporting strategies. We have also tried to limit the export to unary clauses (line size=1) like most current portfolio solvers do, but this does not lead to good performance, since only 177 instances are solved.

Let us now focus on the restart strategy. Quite obviously, the "luby" technique obtains overall worst results than the "lbd " one. This clearly shows the particular interest of this lbd concept introduced in [START_REF] Audemard | Predicting learnt clauses quality in modern SAT solvers[END_REF]. About import strategy, no clear winner appears when looking at the results in Table 1. Indeed, the best results in term of number of solved SAT instances is obtained with no freeze (97) when associated with the "luby" restart and the "size limit" export strategy, whereas the best number of solved UNSAT instances is obtained with the "freeze" strategy (113). Furthermore, no freeze enables to obtain the best overall result solving 205 instances out of the 300 used ones. Hence, it would be audacious to plead for one of the 3 proposed techniques. However, a large number of our proposed policies performs in practice better than "classical" clause exchange techniques, represented in Table1 by ManySat.

In a second experiment, we wanted to assess the behavior of the solver when using some of our proposed policies. To this end, we have conducted the exact same experiments than the one presented in Section 3; the obtained results are reported in the Figure 2. First, we have tried with size limit, luby, and no freeze policies (denoted SLN, see Figure 2(a)). Clearly, this version behaves very well, since most of the dots are located under the diagonal. Moreover, for most instances, #usedSC+#unused(SC) #SC is close to 1 (dots near the second diagonal), which indicates that the solver does not carry useless clauses without deleting them. Most of them proves useful, and the other ones are deleted.

Then, the experimentation was conducted with the lbd limit, lbd and freeze combo (denoted LLF, see Figure 2(b)). At first sight, the behavior is here less satisfying than the SLN version, since for most instances at least half of imported clauses are deleted without being from any help. Actually, in this version, a much larger number of clauses are exported due to the "lbd limit" export policy, which leads to a lower rate of useful clauses. Fine-tuning parameters (lbd limit values, number of time a clause has to be frozen before being permanently deleted, etc.) might improve this behavior.

Looking at some detailled statistics provided in Table 2, it indeed appears that the LLF version shares a lot more clauses than the SLN one (column nb u ). Note that this Table contains some other very interesting information. For instance, it enables to see that for some benchmarks (e.g. AProVE07-21), about 90% of imported clauses are actually frozen and do not immediately participate to the search, whereas for other instances, we face the opposite situation (hwmcc10...) with only 10% of clauses that are frozen when imported. This reveals the high adaptability of the psm measure. Let us focus now on the number of imported clauses, compared to the number of conflicts needed to solve the instance. The SLN version produces very often more conflict clauses than it imports from other working threads (nb c /nb i < 1), even though this is not true with some benchmarks (e.g. AProVE07-21, hwmcc10...). Note that the nb c /nb i rate of the LLF version exhibits a very high variability, from 0.58 for the smallest value in Table 2 (velev-pipe-o-uns...) to more than 4, meaning that in such cases, each time the solver produces a conflict (and consequently a clause), it imports more than 4 clauses on average. Let us also emphasize that the computationnal cost of the psm measure is not major (see "psm time" column). During all our experiments, PeneLoPe have spent at most 5% of the solving time to compute psm.

On a more general view, even if the no-freeze policy seems to be the best in terms of efficiency in communication between threads of the solver, it has the disadvantage of adding every imported clause in the set of active clauses. This leads to a lower number of propagation per second until the next re-examination of the whole clause database. This might be a problem if we want to increase the number of threads of the solver. On the other hand, the freeze-all policy does not slow down the solver. Yet, such solver is not able to use the imported clauses as soon as they are available, and therefore explores subspaces that would have been pruned with the no-freeze policy. 2. Statistics about some unsatisfiable instance solving. For each instance and each version, we report the WC time needed to solve it, the number of conficts (nbc, in thousands), the number of imported clauses (nbi, in thousands) with between brackets the rate between nbi and nbc, the percentage of clauses frozen at the import (nb f ), the percentage of useful imported clauses (nbu) and the percentage of unused deleted clauses (nb d ). Finally, we provide the rate of time (w.r.t. the overall solving time) spent on computing the psm value. Except for time, we compute the average between the 8 threads for these statistics.

Comparison with state of the art solvers

In this Section, we propose a comparison of two of our proposed prototypes against state-of-the-art parallel SAT solvers. We have selected solvers that prove the most effective during the last competitive events: ppfolio [START_REF] Roussel | [END_REF], cryptominisat [START_REF] Soos | Cryptominisat[END_REF], plingeling [START_REF] Biere | lingeling[END_REF] and ManySat [START_REF] Hamadi | Manysat: a parallel SAT solver[END_REF].

For PeneLoPe, we choose for both versions the lbd restart strategy and the lbd limit for the export policy. These two versions only differ from their import policies: freeze and no freeze. Let us precise that contrary to previous experiments, we do not use the deterministic mode in these experiments, in order to obtain the best possible performance.

Figure 3 shows the obtained results through different representations; Table 3(a) provides the number of solved instances for the different solvers, Figure 3(b) details the comparison of PeneLoPe and Plingeling through a scatter plot, and a cactus plot in Figure 3(c) gives the number of solved instances w.r.t. the time (in seconds) needed to solve them. PeneLoPe outperforms all other parallel solvers; indeed, it succeeds to solve 216 instances while no other solver is able to exceed 200 (Table 3(a)). Note that only considering SAT instances, the best results come from plingeling which solves 99 instances. This is particularly noticeable in Figure 3(b) where PeneLoPe and plingeling are more precisely compared; indeed, most of "SAT dots" are located above the diagonal, illustrating the strength of plingeling on these instances. How- In addition, we have compared the same solvers on a 32 cores architecture. More precisely, the considered hardware configuration is now Intel Xeon CPU X7550 (4 processors, 32 cores) 2.00GHz with 18 MB of cache and a RAM limit of 256GB. The software framework is the same as with previous experiments. Each solver is run using 32 threads, and the obtained results are displayed in Figure 4 in a similar way than previously. First, let us remark that except for plingeling, all solvers improve their results when they are run with a larger number of threads. The benefit is limited for certain solvers, however. For example, cryptominisat solves 193 instances with 8 threads, and 201 instances with 32 threads. The improvement is stronger with PeneLoPe whose both versions solve 15 extra instances when 32 threads are used, and especially for ManySAT with a gain of 29 instances. The gap can be more remarkable looking at the cactus plot in Figure 4(c), since our 3 competitors solve about the same number of instances within the same time (curves very close to each other), whereas the curve of PeneLoPe and ManySAT clearly shows their ability to solve a larger number of instances within a more restricted time. Besides, it is worth noting that PeneLoPe solves the same number of instances as Plingeling, ppfolio and cryptominisat with a (virtual) time limit of only 400 seconds. Finally, we can also notice than PeneLoPe can be improved on SAT instances. Indeed, it appears that Luby restarts are more efficient for SAT than for UNSAT, whereas the exact opposite phenomenon happens for UNSAT instances with the lbd restart strategy.

Adding computing units has different impacts. For instance, for ppfolio and plingeling the gain is not major, since augmenting the number of working threads "just" improves the number of CDCL sequential solvers that explore the search space; each worker does not benefit from the exploration of the other ones, since with these solvers, little (if any) collaboration is done. PeneLoPe benefits more from more computing units because the number of exchanged clauses coming from different search subspaces is greater. This leads to a wider knowledge for each thread without being slowed down too much, thanks to the freezing mechanism.

Finally, let us emphasize that during all our experiments with PeneLoPe, all working threads share the exact same parameters and strategies, just like in our preliminary experimentation in Section 3. Improving diversification in the different sequential CDCL searches should probably boost even more our case study solver.

Conclusion

In this paper, we have proposed new strategies to manage clause exchange within parallel SAT solvers. Based on the recent psm and lbd concepts, the idea is to adopt different strategies for import and export of clauses. We have carrefully studied different empir-ical aspects of our proposed ideas and compared our solver to best known parallel SAT engines, showing that it appears to be a highly competitive prototype.

Clearly, diversifying the different working threads should improve the performance of our case study solver PeneLoPe, since this technique is known to be the cornerstone of the efficiency of some portfolio solvers, like ppfolio. We plan to study this point in the next future.

Fig. 1 .

 1 Fig. 1. Comparison between useful share clauses and unused deleted clauses. Each dot corresponds to an instances. x-axis gives the rate of useful shared clauses #used(SC)/#SC, whereas the y-axis gives the rate of unused deleted shared clauses #unused(SC)/#SC.

Fig. 2 .

 2 Fig. 2. Comparison between usefull share clauses and useless deleted clauses. Each dot corresponds to an instances. x-axis gives the rate of useful shared clauses #used(SC) #SC , whereas the

Fig. 3 .

 3 Fig. 3. Comparison on 8 cores

Fig. 4 .

 4 Fig. 4. Comparison on 32 cores

  PeneLoPe VS state-of-the-art parallel solvers

	Solver	#SAT	#UNSAT	#SAT+#UNSAT
	PeneLoPe freeze	104	127	231
	PeneLoPe no freeze	99	131	230
	ManySAT [10]	105	111	216
	ppfolio [16]	107	97	204
	cryptominisat [18]	96	105	201
	Plingeling [4]	100	95	195
	(a)

This work has been supported by CNRS and OSEO, under the ISI project "Pajero".

All experimentations of this paper have been conducted on a dual socket Intel XEON X5550 quad-core 2.66 GHz with 8 MB of cache and a RAM limit of 32GB, under Linux CentOS 6 (kernel 2.6.32). All solvers use 8 threads. The timeout was set to 1200 seconds WC for each instance. If no answer was delivered within this amount of time, the instance was considered unsolved. We used the application instances (300) of the SAT competition 2011.

http://www.cril.fr/ ˜hoessen/penelope.html

in reference to Odysseus's faithful wife who wove a burial shroud, linking many threads together


Time to go augmented in vascular interventional neuroradiology?

René Anxionnat 1 , Marie-Odile Berger 2,3 , and Erwan Kerrien 2,3

1 Therapeutic and Diagnostic Interventional Neuroradiology Dept, Univ. Hospital, Nancy, F-54000, France 2 Inria, Villers-lès-Nancy, F-54600, France, 3 Université de Lorraine, Loria, UMR7503, Vandoeuvre-lès-Nancy, F-54600, France

This editorial paper reports on our experience in introducing augmented reality (AR) in interventional neuroradiology environments. Our expectations about the next AR tools, in particular for more advanced visualization, are also put forward. For practical reasons, the references will be restricted to our contributions. For further information, the last recommendations concerning the medical management of aneurysm induced hemorrhages can be found in [START_REF] Connolly | Guidelines for the management of aneurysmal subarachnoid hemorrhage[END_REF].

Interventional neuroradiology

Interventional neuroradiology is a medical discipline that leverages minimally invasive techniques to operate on vascular lesions of the nervous system. The treatment is performed through the inside of the blood vessels, using medical imaging as visual feed-back. Such endovascular procedures are mainly performed to treat aneurysms. Intracranial aneurysms are sacciform ectasias of arteries located on the brain surface. The main associated risk is their rupture, leading to an hemorrhage with dramatic clinical consequences. Their size (diameter) varies between 2 mm and a few tens of millimeters. An endovascular treatment (EVT) progressively occludes the aneurysm with very soft spiral-like coils. EVTs were introduced in the 60's but really took off in the 90's after controlled detachable coils were developed. EVT has now replaced neurosurgery as the first choice treatment of aneurysms.

EVTs are performed in interventional vascular operating rooms where X-ray imaging enables the precise analysis of the lesions and their treatment. X-ray Angiography still remains the imaging modality of reference thanks to its optimal spatial and temporal resolution. The endovascular navigation followed by the EVT itself are performed under the real-time visual feed-back of a low dose and high frame rate (15 fps on average) angiography image acquisition called fluoroscopy. However, these low quality images are projection images that do not contain any 3D information. Several viewpoints are required for an easier guidance through complex vascular networks and a better control of the treatment. Therefore aneurysm EVT are usually performed in biplane mode, providing simultaneous Antero-Posterior (AP) and Lateral (Lat) fluoroscopic views. No significant improvements were brought in the last few years in the control of EVTs using fluoroscopy. The development of Augmented Fluoroscopy very re-cently modified this status by introducing, for the first time, Augmented Reality in vascular interventional neuroradiology.

Augmented Fluoroscopy: principle and clinical interest

The idea of enriching fluoroscopy images with 3D data was born shortly after the development, in 1997, of 3D rotational angiography (3DRA) [START_REF] Anxionnat | 3D angiography. clinical interest. first applications in interventional neuroradiology[END_REF], a cone-beam tomography reconstruction techniques that produces a volume from angiography images acquired during a rotation of the vascular C-arm. 3DRA allows for an optimal treatment planning thanks to a precise analysis of the aneurysm morphology: its size, its shape and its neck, where it connects with its parent vessel [START_REF] Anxionnat | Intracranial aneurysms: Clinical value of 3D digital subtraction angiography in the therapeutic decision and endovascular treatment[END_REF]. From 3DRA, a working view can be defined that best identifies the aneurysmal neck and clearly reveals the limits for the coil positioning. 3DRA rapidly became a must-have imaging modality for EVT planning, to improve treatment safety and expand their indications. However, over a decade was necessary to actually integrate 3DRA with fluoroscopy thereby building the first augmented reality tool suitable for use in clinical practice.

During EVT, superimposing 3DRA onto the fluoroscopy sequence provides the physician with a stereoscopic vision of the morphology of vascular bifurcations, of the aneurysm and its relations with neighboring vessels. Endovascular guidance is made easier and coil deployment is better controlled.

Augmented Fluoroscopy (AF) is based on 3D/2D registration between 3DRA and fluoroscopy in any C-arm orientation. A prototype was developed in close collaboration between the research team (Inria Nancy Grand-Est), the manufacturer (GE Healthcare) and the medical staff (Department of Neuroradiology University Hospital of Nancy, France). The geometric accuracy of the implemented machine-based registration was first measured [START_REF] Gorges | Model of vascular C-arm for 3D augmented fluoroscopy in interventional radiology[END_REF]. The next step consisted in further evaluating the prototype in the clinical conditions of an aneurysm EVT. Validation criteria were designed to address the clinical requirements met in the operating room, in terms of geometric accuracy and visualization. Visualization should indeed both preserve the visibility of the EVT tools (microcatheters, guidewires, and coils) and clearly depict the vascular topology in 3D.

The geometric accuracy was first estimated on a silicon phantom of the cerebral vasculature under various orientations of the C-arm. It was proved to be less than 0.5 mm and therefore compatible with the clinical objective [START_REF] Gorges | 3D augmented fluoroscopy in interventional neuroradiology: precision assessment and first evaluation in clinical cases[END_REF]. This first conclusion was confirmed on clinical cases.

Concerning visualization, we chose to blend the 3DRA volume in Volume Rendering onto the fluoroscopic images. Easy to implement, this solution presents as a further advantage that it barely impacts the usual physician's environment (see Figure 1). Using AF in clinical conditions confirmed the relevance of this choice, and helped to significantly improve this prototype with functionalities such as interactive tuning of the vessel transparency to reach an optimal consensus between vascular relief and envovascular material visibility. After these successive improvements, AF was launched as a product in 2007. 3 The ordeal of going into clinical practice: an under-estimated step

The medical team was involved in the development of AF right from the start, and the preliminary evaluation demonstrated its definite clinical interest. Nevertheless, several limitations made the integration of AF in clinical routine very gradual. First, AF is only available on the AP C-arm. Yet, in biplane mode, the working view used for the EVT may only be reached by the Lat C-arm. Second, in actual clinical practice, many events may cause the machine-based registration to degrade which quite often calls for a manual correction in the absence of an image-based registration adjustment. Moreover, the AF monitor was first set aside in the operating room in order to minimize the perturbation on the otherwise unchanged environment. On one hand, the physicians readily accepted such a discrete modification in their work environment. On the other hand, the prototype was underutilized. Therefore, significant improvements, in terms of ergonomics, were made to better integrate the prototype into the operating room, such as larger zoom factors and an actual integration as part of the panel of control monitors.

The second step towards the use in clinical routine was gradual and more or less fast depending on physicians. Indeed, physicians needed some time to agree to change their work routine either during risky interventions that required a lot of concentration or for cases they could easily treat without AF. But this phase, including, and especially for the latter simple cases, proved essential to the evaluation by physicians who had to become familiar with the new environment and compare it with reference tools, namely casual fluoroscopy that was still available. Once AF was mastered, the physician could use it in complex cases and rely on information that would not be accessible with mere fluoroscopy, e.g. axial views of complex aneurysms. AF is being used in clinical routine at our institution since 2011. Arteriovenous malformations (AVMs) are scarcer than brain aneurysms and also differ a lot on both the morphology and therapy levels. They consist of a network of abnormal vessels interposed between arteries and veins which creates a high blood speed arteriovenous shunt in the brain parenchyma. The treatment is to occlude the AVM using fluid or pasty injections after a distal navigation within a very small, sub-millimetric, highly branched vascular network. Technological advances in the field of navigation tools and endovascular material allow to perform such embolization in very distal vascular areas, as well as highly functional brain regions.

AF can facilitate this complex navigation by displaying the origin and path of afferent arteries and differentiating them from neighboring vessels or vessels that superimpose in the fluoroscopic view. These clinical needs are more demanding than for aneurysms given the complexity and finesse of the vascular network. Additional work in terms of accuracy of registration, and vascular segmentation and visualization will be necessary to make this tool functional in clinical practice.

During an EVT, the physician can only see vessels on the monitors, but has no access to a direct visualization of the cerebral parenchyma in the surroundings of the endovascular material. Locating crucial functional brain areas cannot be realized but through a mental effort to relate a priori anatomical knowledge and preoperative imaging to intraoperative views. The inherent inaccuracy of such process may lead the physician to excessively embolize in highly functional areas, potentially causing dramatic complications, or, conversely to give up treatment in case of doubt. A multimodal localization is definitely required, especially combining MRI and angiography, to identify the cerebral regions with a high accuracy. Innovative visualization tools will have to be developed to setup such new multimodality environments and bring relevant information, in an intuitive way, to the physician during the treatment.

During the treatement, AF provides 3D vascular information in any orientation the C-arm can reach. As such, a real progress was made compared to mere fluoroscopy imaging. However, endovascular material still is only visible under projection in limited orientations. The next step will see the 3D reconstruction of endovascular tools and material during the EVT. These tools and material will be directly located in the 3DRA volume and thereby, on one hand, visible in any view, including virtual views, such as axial views inaccessible to the C-arm, and on the other hand, easy to relate to any 3D multimodal imaging volume. Very hard technical and scientific issues will have to be overcome, but it casts a glimpse of potentially dramatic breakthroughs in the way EVTs are performed.

Having such a possibility will allow for a better control of the EVT, thus improving safety. However working in a multimodal environment will generate inaccuracies due to the involved registration and segmentation processes, that will need to be quantified and that the physician should be fully aware of. The physician will have to agree to cope with this uncertainty when working on virtual views without the direct control provided by fluoroscopy, and thus no possibility for correction. An important intellectual investment will be necessary to learn how to use these tools and manage this uncertainty before appropriating these tools in clinical practice.

Eventually, future augmented environments will be enriched not only with visual information from other imaging modalities such as functional, but also with other data such as generated by hemodynamic simulation or wall pressure computations for aneurysms.

Conclusion

Our experience with AF shows it is possible to develop Augmented Reality tools in the field of interventional neuroradiology. But there is a long way between the initial idea and the product used in clinical practice: 10 years in the case of AF.

For this tool to be used it must meet specific clinical needs, clearly identified by physicians, and be validated for this purpose. This validation must meet specific criteria and objectives. In the case of an EVT, which corresponds to a risky procedure requiring a high concentration from the physician, any Augmented Reality tool must be fully integrated into the operating room and provide an intuitive interface.

It is important that any operator that was not necessarily involved in the development and validation process, be persuaded to use the tool first in simple cases where it can be evaluated within a personal operating environment so as to gradually become more familiar with the tool and finally trust the additional information it provides. Under these conditions the augmented environment has the potential to bring real benefits to the physician, especially in complex cases, and imply actual changes in the clinical practice. As an example, AF provides actual 3D information which biplane fluoroscopy useless for most interventions and thus reduceing patient irradiation and exam time while probably improving the safety of the intervention.

AF has paved the way for Augmented Reality in interventional neuroradiology. A vast field of opportunities exist to adapt this tool to other, more demanding, clinical applications and develop new Augmented Reality tools. New angiographic rooms will emerge that integrate an augmented environment, allowing the interventional neuroradiologist to work in fully multimodal setup enriched with visual, and other kinds of, information.

Fig. 1 .

 1 Fig. 1. Augmented Fluoroscopy (AF) case. (left) Original fluoroscopy image ; (right) AF view. AF offers a much clearer depiction of the ruptured aneurysm to be treated (green circle), and also unveils a microscopic incidental aneurysm which hampers the guide wire navigation (red arrow).