Satisfiability Modulo Theories (SMT) is the problem of deciding a quantifier-free formula modulo a background theory T. State-of-the-art SMT-Solvers are based on the DPLL(T) model, which efficiently combines a DPLL SAT-Solver, used to handle disjucntive choices, and a Theory Solver, a decision procedure for T, used to solve conjunctions of constraints. In this lecture we review the DPLL approach to SAT and extend it to DPLL(T) approach. Also we examine some useful theories, commonly used in the formal analysis of software, by sketching the main ideas behind the algorithms used to solve them.