Starting SAT solver papers
An excellent beginner overview is given by the following article from 2009.


Boolean Satisfiability: From Theoretical Hardness to Practical Success, Sharad Malik, Lintao Zhang,  Communications of the ACM, 2009


There are several ways to get into the technical aspects. You can even start with the original Davis-Putnam paper. It is extremely clear and has detailed examples. When discussing SAT optimizations in a course, we discovered that a few one  may imagine are already there. The Davis-Logeman-Loveland paper is (I feel) less instructive, but it is so short you may as well read it. 


A Computing Procedure for Quantification Theory, Martin Davis, Hilary Putnam, Journal of the ACM, 1960.
A machine program for theorem-proving, Martin Davis, George Logemann, Donald Loveland, Communications of the ACM, 1962.


There are may ways to catch up on the developments of the next 50 years. I would recommend lecture slides. Just searching for 'DPLL' will throw up many many tutorials. If you browse through them, I'm sure the mist will clear -- to some extent. There are also many useful surveys. The Zhang-Malik paper is a good place to start. There are several articles in the Handbook of Satisfiability you may find useful. 


The Quest for Efficient Boolean Satisfiability Solvers, Lintao Zhang, Sharad Malik, Joint invited paper for CAV and CADE 2002.
Handbook of Satisfiability, Edited by Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh, 2009
Anatomy and Empirical Evaluation of Modern SAT Solvers, Karem  Sakallah, Joao Marques-Silva, Bulletin of the EATCS, 2011.


I second the suggestion of Mikolaos. The MiniSAT code is clean and of manageable size. You can play with it. There are several other solvers you can try. CryptoMiniSat is also quite clean. You should also consult the work of Armin Biere, who writes SAT solvers and writes about writing SAT solvers.