zbMATH — the first resource for mathematics

Boosting local search thanks to cdcl. (English) Zbl 1306.68138
Fermüller, Christian G. (ed.) et al., Logic for programming, artificial intelligence, and reasoning. 17th international conference, LPAR-17, Yogyakarta, Indonesia, October 10–15, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-16241-1/pbk). Lecture Notes in Computer Science 6397, 474-488 (2010).
Summary: In this paper, a novel hybrid and complete approach for propositional satisfiability, called SatHys (Sat Hybrid Solver), is introduced. It efficiently combines the strength of both local search and cdcl based sat solvers. Considering the consistent partial assignment under construction by the cdcl SAT solver, local search is used to extend it to a model of the Boolean formula, while the cdcl component is used by the local search one as a strategy to escape from a local minimum. Additionally, both solvers heavily cooperate thanks to relevant information gathered during search. Experimentations on SAT instances taken from the last competitions demonstrate the efficiency and the robustness of our hybrid solver with respect to the state-of-the-art cdcl based, local search and hybrid SAT solvers.
For the entire collection see [Zbl 1197.68008].

68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
SATzilla; UnitWalk
Full Text: DOI