5 of 6 added 40 characters in body

DPLL time complexity analysis

Consider the most naïve backtracking for CNF-SAT. It only checks if an assignment satisfies the input formula $\phi$ when all the $n$ variables have values assigned. Let $m$ be the size of $\phi$. Then the time complexity for this backtracking is $O(m 2^n)$.

Now, consider DPLL. This algorithm is just a simple backtracking with some pruning strategy. Besides, DPLL simplifies $\phi$ along the backtracking, instead of doing it only at once, so the $O(m)$ cost is amortized. Hence, its running time should also be $O(m 2^n)$. Still, some places state that $O(2^n)$ is also an upper bound for DPLL (Wikipedia, for example). Does anybody knows the analysis to find this upper bound?