Integrating Conflict Driven Clause Learning to Local Search

TL;DR

This paper presents SatHyS, a hybrid SAT solver combining local search and conflict driven clause learning, which improves performance on various SAT instances by switching strategies at local minima.

Contribution

It introduces a novel hybrid approach that integrates local search with CDCL, effectively handling both SAT and UNSAT problems within a unified framework.

Findings

Good performance on SAT instances from recent competitions

Effective switching between local search and CDCL at local minima

Improved handling of MUS in UNSAT problems

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.