Using failed local search for SAT as an oracle for tackling harder A.I. problems more efficiently?

Abstract. Local search is often a suitable paradigm for solving hard decision problems and approximating computationally difficult ones in the artificial intelligence domain. In this paper, it is shown that a smart use of the computation of a local search that failed to solve a NP-hard decision problem A can sometimes slash down the computing time for the resolution of computationally harder optimization problems con-taining A as a sub-problem. As a case study, we take A as SAT and consider some PNP [O(logm)] symbolic reasoning problems. Applying this technique, these latter problems can often be solved thanks to a small constant number of calls to a SAT-solver, only