The satisfiability problem is the problem of deciding for a given propositional formula whether it has a satisfying assignment. The video introduces, motivates, and illustrates this problem, and presents two algorithms for solving it, namely propositional resolution and the DPLL algorithm.
