
## 7 Conclusion

In this paper a new integration of local search and CDCL based SAT solvers is introduced. This hybrid solver represents an original combination of both engines. The CDCL component can be seen as a new strategy for escaping from local minimum. This is achieved by the assignment of opposite literals from the falsified clause. In the case of satisfiable SAT instances, such assignments are supposed to behave like a tabu search approach, whereas for unsatisfiable ones, they try to focus on a small sub-part of the formula, which is minimally unsatisfiable (MUS). SATHYS, the resulting method, obtains very good results for a large category of instances. This new method can be improved in different ways. As it was pointed in the experimental section, our solver allows for more diversification and less intensification.

First attempts have been done to correct this. Finally, we aim at designing a solver which would focuses only on an approximation of the MUS.

## References

[1] B. B. & Fr¨ohlich (2004): *WalkSAT as an Informed Heuristic to DPLL in SAT Solving.* Technical Report, CSE
573 : Artificial Intelligence.

[2] A. Balint, M. Henn & O. Gableske (2009): *A novel approach to combine a SLS- and DPLL-solver for the* satisfiability problem. In: proceedings of SAT.

[3] R. Battiti & M. Protasi (1997): *Reactive search, a history-sensitive heuristic for MAX-SAT*. J. Exp. Algorithmics 2, p. 2.

[4] A. Biere, M. Heule, H. van Maaren & T. Walsh, editors (2009): *Handbook of Satisfiability*, Frontiers in Artificial Intelligence and Applications 185. IOS Press.

[5] J. Crawford (1996): *Solving Satisfiability Problems Using a Combination of Systematic and Local Search*.

In: Second Challenge on Satisfiability Testing organized by Center for Discrete Mathematics and Computer Science of Rutgers University.

[6] M. Davis, G. Logemann & D. Loveland (1962): *A machine program for theorem-proving*. Communication of ACM 5(7), pp. 394–397.

[7] N. E´en & A. Biere (2005): Effective Preprocessing in SAT Through Variable and Clause *Elimination*. In:
proceedings of SAT. pp. 61–75.

[8] N. Een & N. S¨orensson (2003): *An Extensible SAT-solver*. In: proceedings of SAT. pp. 502–518.

[9] E.Gregoire, B. Mazure & C. Piette (2006): *Tracking MUSes and Strict Inconsistent Covers*. In: Sixth ACM/IEEE International Conference on Formal Methods in Computer Aided Design(FMCAD'06). San Jose
(USA), pp. 39–46.

[10] H. Fang & W. Ruml (2004): *Complete Local Search for Propositional Satisfiability*. In: proceedings of AAAI. pp. 161–166.

[11] L. Fang & M. Hsiao (2007): *A new hybrid solution to boost SAT solver performance*. In: proceedings of DATE. pp. 1307–1313.

[12] F. Glover (1989): *Tabu search - Part I*. ORSA Journal of Computing , pp. 190–206. [13] E. Gregoire, B. Mazure & C. Piette (2006): *Extracting MUSes*. In: proceedings of ECAI. pp. 387–391.

[14] E. Gregoire, B. Mazure & C. Piette (2007): *Boosting a Complete Technique to Find MSS and MUS thanks to* a Local Search Oracle. In: International Joint Conference on Artificial Intelligence(IJCAI'07). Hyderabad
(India), pp. 2300–2305.

[15] E. Gregoire, B. Mazure & C. Piette (2007): *Local-Search Extraction of MUSes*. Constraints 12(3), pp.

325–344.