Boosting complete techniques thanks to local search methods

In this paper, an efficient heuristic allowing one to localize inconsistent kernels in propositional knowledge-bases is described. Then, it is shown that local search techniques can boost the performance of logically complete methods for SAT. More precisely, local search techniques can be used to guide the branching strategy of logically complete techniques like Davis and Putnam's one, giving rise to significant performance improvements, in particular when addressing locally inconsistent problems. Moreover, this approach appears very competitive in the context of consistent SAT instances, too.