The planning problem in Artificial Intelligence was the first application of SAT to reasoning about transition systems and a direct precursor to the use of SAT in a number of other applications, including bounded model-checking in computer-aided verification.

This chapter presents the main ideas about encoding goal reachability problems as a SAT problem, including parallel plans and different forms of constraints for speeding up SAT solving, as well as algorithms for solving the AI planning problem with a SAT solver. Finally, more general planning problems that require the use of QBF or other generalizations of SAT are discussed.