DPLL (for Davis, Putnam, Logemann, and Loveland) algorithms form the largest family of contemporary algorithms for SAT (the propositional satisfiability problem) and are widely used in applications. While the behavior of DPLL algorithms on unsatisfiable formulas has been extensively investigated (by studying the refutation size in Resolution proof system), little research was done towards proving lower bounds on satisfiable instances. We fill this gap by constructing satisfiable formulas which are provably difficult for a wide class of DPLL algorithms. In the second part of the talk I will survey some lower bounds on other restricted computational models, which include a generalization of our results for backtrack SAT algorithms and proving integrality gaps for Lovasz-Schrijver hierarchy for the linear relaxations of a (hypergraph) vertex cover. The talk is based on joint work with Edward Hirsch, Dmitry Itsykson, Allan Borodin, Joshua Buresh-Oppenheim, Russell Impagliazzo, Avner Magen, Toniann Pitassi, Sanjeev Arora, and Iannis Tourlakis