The advancements made in the last decade in algorithms for Boolean Satisfiability (SAT) motivated the application of SAT solvers in different areas of Computer Science and Engineering, including theorem proving, artificial intelligence, verification of reactive systems, design automation, cryptography, among others. In the area of reactive systems verification, the most well-known utilization of SAT is in model checking. The objective of this talk is to survey the utilization of SAT models and algorithms in model checking. The talk will emphasize the utilization of SAT models and algorithms in two specific contexts: bounded and unbounded model checking.