SAT  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.). 
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.
 Davis Putnam algorithm, Wikipedia
 Resolution in logic, Wikipedia
 Davis Putnam Logemann Loveland algorithm, Wikipedia