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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.5.5 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |