arXiv · 0910.1247
Integrating Conflict Driven Clause Learning to Local Search
Abstract
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.
Explore related subjects
Keep this discovery
Gilles Audenard, Jean-Marie Lagniez, Bertrand Mazure, Lakhdar Saïs. 2009-10-07. Integrating Conflict Driven Clause Learning to Local Search. https://doi.org/10.4204/eptcs.5.5
Cite the original work for its findings. Save a collection to share your selection of sources.