I'm looking at the Davis-Putnam algorithm. I don't understand how resolution results in an exponential blowup in the size of the formula, since it seems that after each step, the size is reduced.
$(l_1\lor l_2\lor p)\land (k_1\lor k_2\lor \lnot p)$ becomes $(l_1\lor l_2\lor k_1\lor k_2)$.
$$(l_1 \lor p) \land (l_2 \lor p) \land (k_1 \lor \neg p) \land (k_2 \lor \neg p)$$
becomes
$$(l_1 \lor k_1) \land (l_1 \lor k_2) \land (l_2 \lor k_1) \land (l_2 \lor k_2).$$
In general, if you had $k$ clauses of the form $(\cdots \lor p)$ and $k$ clauses of the form $(\cdots \lor \neg p)$, you would obtain a formula with $k^2$ clauses, so the number of clauses in the formula is roughly squared. Repeat this multiple times, roughly squaring each time, and you might obtain an enormous blowup (in fact, exponential).