
| Crafted   | Industrial   | Random   |       |     |       |     |
|-----------|--------------|----------|-------|-----|-------|-----|
| sat       | unsat        | sat      | unsat | sat | unsat |     |
| ADAPTG2   | 326          | 0        | 232   | 0   | 1111  | 0   |
| RSAPS     | 339          | 0        | 226   | 0   | 1071  | 0   |
| WSAT      | 259          | 0        | 206   | 0   | 1012  | 0   |
| CLS       | 235          | 75       | 227   | 102 | 690   | 0   |
| SATHYS    | 322          | 191      | 466   | 309 | 341   | 14  |
| HYBRIDGM  | 290          | 0        | 209   | 0   | 1114  | 0   |
| HYBRID1   | 329          | 0        | 277   | 0   | 1126  | 0   |
| MINISAT   | 402          | 369      | 588   | 414 | 609   | 315 |

Table 1 summarizes the obtained results on this large number of instances. For more details on this experimental part, the reader can refer to http://www.cril.fr/∼lagniez/sathys. For each category and for each solver we report the number of solved instances. Of course, MINISAT a state-ofthe-art CDCL based complete solver is only considered to mention the gap between local search based techniques and complete modern SAT solvers on industrial and crafted instances. On random satisfiable instances, local search techniques generally outperform complete techniques.

Before analysing more precisely the table of results (Table 1), remark that only three solvers are able to solve unsatisfiable instances (MINISAT, CLS and SATHYS). The recent hybrid methods submitted at the last SAT competition cannot prove inconsistency in the allowed time.

On the crafted instances, SATHYS is very competitive and solves approximately the same number of satisfiable instances as RSAPS, ADAPTG2 and the recent hybrid methods. Furthermore, SATHYS solves much more instances than WSAT, its built-in solver. Concerning unsatisfiable crafted instances, as expected our approach is less efficient than MINISAT but it is proved highly more efficient than CLS.

Concerning industrial instances, SATHYS solves two times more satisfiable instances than SLS and hybrid methods. Once again, on unsatisfiable industrial instances, your solver is better than CLS but less efficient than MINISAT.

These results show that conflict analysis allows to solve efficiently structured SAT and UNSAT instances.

Finally, for the random category, we can note that SATHYS is unable to solve unsatisfiable problems.

As pointed by MINISAT results, learning is not the good approach to solve random instances. As a summary, unfortunately our approach cannot reach the minisat performance. However the solver SATHYS
is much more efficient than local search based algorithms and hybrid methods. It significantly improves WSAT, its built-in solver. Even if MINISAT is the best solver on crafted and industrial instances, these first results are very encouraging and reduce the gap between local search based techniques and DPLL-like complete solvers.

The figures 3, 4 and 5 give the classical cactus plot. For each tested method, the X-axis corresponds to the number of formulas and the Y-axis corresponds to the time needed to solve them if they were ran in parallel. When a method does not appear in the curve, that means that this method is not able to solve instance of this instances category. In these figures, we have distinguished satisfiable and unsatisfiable instances for each categories.