Integrating Conflict Driven Clause Learning to Local Search

Gilles Audenard
(Université Lille-Nord de France)
Jean-Marie Lagniez
(Université Lille-Nord de France)
Bertrand Mazure
(Université Lille-Nord de France)
Lakhdar Saïs
(Université Lille-Nord de France)

This article introduces SatHyS (SAT HYbrid Solver), a novel hybrid approach for propositional satisfiability. It combines local search and conflict driven clause learning (CDCL) scheme. Each time the local search part reaches a local minimum, the CDCL is launched. For SAT problems it behaves like a tabu list, whereas for UNSAT ones, the CDCL part tries to focus on minimum unsatisfiable sub-formula (MUS). Experimental results show good performances on many classes of SAT instances from the last SAT competitions.

In Yves Deville and Christine Solnon: Proceedings 6th International Workshop on Local Search Techniques in Constraint Satisfaction (LSCS 2009), Lisbon, Portugal, 20 September 2009, Electronic Proceedings in Theoretical Computer Science 5, pp. 55–68.
Published: 8th October 2009.

ArXived at: https://dx.doi.org/10.4204/EPTCS.5.5 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org