Figure 3: The Davis-Putnam procedure for checking whether a given formula in CNF is satisfiable.