Algorithms for SAT and upper bounds on their complexity

We survey recent algorithms for the propositional satisfiability problem, in particular algorithms that have the best current worst-case upper bounds on their complexity. We also discuss some related issues: the derandomization of the algorithm of Paturi, Pudlák, Saks and Zane, the Valiant-Vazirani Lemma, and random walk algorithms with the “back button”.