Over the last two decades, we have witnessed a silent revolution in software engineering thanks in part to Boolean SAT and SMT solvers. These tools have made it significantly easier to design, build, and maintain myriad kinds of program analysis, testing, synthesis and verification systems. Further, they have enabled new software engineering methods that were otherwise deemed infeasible. In these lecture notes, we provide an introductory overview of SAT and SMT solvers, from both practical as well as theoretical points of view. Specifically, we describe in detail the architecture of the DPLL, CDCL, and SMT algorithms. Further, we provide theoretical understanding of these solvers through the lens of proof complexity. Finally, we showcase the power of machine learning techniques to fundamentally transform solver design.