How the Abstract DPLL Algorithm Works in SAT Solving
Describing DPLL as a series of state-transition rules is the worst way I've ever seen to aid understanding the algorithm.  The pseudocode provided in the WIkipedia article on DPLL is much easier to understand if you're approaching the algorithm for the first time.

;Algorithm DPLL
;Input: A set of clauses Φ.
;Output: A Truth Value.

function DPLL(Φ)

if Φ is a consistent set of literals
   then return true;
if Φ contains an empty clause
   then return false;
for every unit clause {l} in Φ
   Φ ← unit-propagate(l, Φ);
for every literal l that occurs pure in Φ
   Φ ← pure-literal-assign(l, Φ);
l ← choose-literal(Φ);
return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {not(l)});


Decision literals are the literals returned by the choose-literal function called above.  Annotated literals are just literals that are members of M that are marked in some way so the DPLL implementation can distinguish decision literals from literals added to M by unit propagation.  This marking is for the sake of the backjumping code which must unroll assignments until the one responsible for the current conflict is found and then replace it.

Note that the original DPLL algorithm did not have backjumping in it.  It simply backtracked, either reversing the current assignment or returning false if the algorithm had run out of assignments to try.  Backjumping was a later innovation.

Note also that pure literal assignment isn't usually done in modern SAT solvers that implement some form of DPLL.  It is a fairly expensive check to do in an algorithm expected to recurse and backtrack an exponential number of times and the benefits of doing the check don't outweigh the costs.