Description of resolution algorithm as it applies to SAT

SAT [5] can be solved with resolution definitively, i.e. if the formula has a true assignment, resolution can find it, and if it cant be satisfied, resolution can show that no assignment exists (at least in exponential time/space.). [4]

Is there a good fully-self contained description somewhere of solving SAT with resolution?

The descriptions on Wikipedia of resolution are focused on a single logical operation, not how to use it in an algorithm to solve SAT, and the Davis Putnam algorithm is described mostly in terms of 1st order logic. I am looking for a description of solving SAT with resolution that does not refer to 1st order logic, just in terms of boolean input variables. Online description is preferred if possible. The connection with DPLL would be helpful also.

[1] Davis Putnam algorithm, Wikipedia

[2] Resolution in logic, Wikipedia

[3] Davis Putnam Logemann Loveland algorithm, Wikipedia

-
You could have a look at the presentations by Joao Marques-Silva. One of his talks here at least has both an explanation and an example of resolution. Also, IIRC the Russell & Norvig AI book has a self-contained description too. – Juho Jan 28 '13 at 2:04