A Novel Approach to Combine a SLS- and a DPLL-Solver for the Satisfiability Problem

The paper at hand presents a novel and generic approach on how to combine a SLS and a DPLL solver to create an incomplete hybrid SAT solver. In our approach, the SLS solver gets supported by a DPLL solver to boost its performance. In order to develop the idea behind our approach, we first define the term of a search space partition (SSP) and explain its construction and use. For testing our new approach, which utilizes SSPs, we implemented it in the solver hybridGM, using gNovelty+ and March-ks. After explaining the implementation details, we perform an empirical study on several publicly available benchmarks in order to test the performance of the new hybrid SAT solver. The results indicate a superior performance of hybridGM over gNovelty+, proving our new approach to be worthwhile.