The focus of this chapter is the Davis–Putnam–Logemann–Loveland (DPLL) algorithm for propositional satisfiability. After a high-level presentation of DPLL, it is shown how DPLL can be implemented efficiently using multiple techniques, including watched literals, conflict-driven clause learning (CDCL), random restart, and branching heuristics. Then several challenging problems are presented, which can be effectively solved by SAT solvers (most of them are implementations of DPLL). The chapter concludes with the major techniques for solving the maximum satisfiability problems, including local search methods and the branch-and-bound algorithm.