Boolean SAT

For an introduction to the Boolean satisfiability problem (SAT), watch this, then this. For a bit more detail on the Davis-Putnam-Logemann-Loveland (DPLL) algorithm, read the section titled "The algorithm" on this Wikipedia page.