SAT Oracles, for NP-Complete Problems and Beyond

SAT solvers have been used in many areas, including software product lines [1], as generic engine to solve NP-complete problems since the 2000's [2]. While the raw performances of the solvers to tackle NP-complete problems have been increasing steadily in the past [4], most impressive recent results rely on sophisticated encodings and better interaction with the solver, allowing to solve NP-hard - and even PSPACE-complete - problems. This is the case for core-based MAXSAT solvers for instance [6], and more recently SAT-based QBF solvers [3]. In this talk, I will review the current features found in modern SAT solvers, and how they are used to solve NP-hard problems. I will present a generic approach called RECAR (Recursive Explore and Check Abstraction Refinement) [5] which allows to take advantage of the feedback of the SAT solver to drive the search on a subproblem to prevent when possible memory blowup.