The last decade has witnessed an increasing interest in Propositional Satisfiability (SAT), with a boost in the performances of SAT solvers. More recently, SAT procedures have been successfully used also as basic inference engines of decision procedures for much more expressive problems, like reasoning in modal and description logics, resource planning, temporal reasoning, formal verification of timed systems, formal verification of circuits at an abstract level.
In this tutorial we focus on the latter aspect, and we show how SAT solvers can be correctly and efficiently extended to work with more expressive domains by integrating them with domain-specific procedures. We provide some foundations, and describe techniques to maximize the effectiveness of this integration. We show some examples of implemented procedures in different domains. We indicate some open problems and research directions.