A New Hybrid Solution to Boost SAT Solver Performance

摘要

Due to the widespread demands for efficient SAT solvers in electronic design automation applications, methods to boost the performance of the SAT solver are highly desired. The paper proposed a hybrid solution to boost SAT solver performance in this paper, via an integration of local and DPLL-based search approaches. A local search is used to identify a subset of clauses to be passed to a DPLL SAT solver through an incremental interface. In addition, the solution obtained by the DPLL solver on the subset of clauses is fed back to the local search solver to jump over any locally optimal points. The proposed solution is highly portable to the existing SAT solvers. For satisfiable instances, up to an order of magnitude speedup can be obtained via the proposed hybrid solver