How the Abstract DPLL Algorithm Works in SAT Solving

Question

I have come across many definitions of the DPLL algorithm but haven't been able to follow them. The ones that are closest to making sense to me are the ones based on state-transition systems with transition rules such as defined here:

$F$ is a CNF formula, $C$ is a clause, and $M$ is a model. A description of it is as follows:

Here, a DPLL procedure will be modeled by a transition system: a set of states together with a relation, called the transition relation, over these states. States will be denoted by (possibly subscripted) $S$.... A state is either fail or a pair $M \parallel F$, where $F$ is a finite set of clauses and $M$ is a sequence of annotated literals.... We will not go into a complete formalization of annotated literals; it suffices to know that some literals $l$ will be annotated as being decision literals; this fact will be denoted here by writing $l^d$ (roughly, decision literals are the ones that have been added to $M$ by the Decide rule given below). Most of the time the sequence $M$ will be simply seen as a set of literals, denoting an assignment, i.e., ignoring both the annotations and the fact that $M$ is a sequence and not a set.

I understand that a literal is an atom or its negation, but I don't understand what an annotated literal is, which is a core part of understanding what a model $M$ is in $M \parallel F$. I also don't understand what the decision literals are.

Two examples are as follows.

This is as much as I can gather. This:

$$\emptyset \parallel 1 \lor \bar{3}, \bar{1} \lor \bar{4} \lor 5 \lor 2, \bar{1} \lor \bar{2}$$

Is essentially an implementation of this:

$$M \parallel F$$

Also, the commas are really $\land$, as in:

$$\emptyset \parallel (1 \lor \bar{3}) \land (\bar{1} \lor \bar{4} \lor 5 \lor 2) \land (\bar{1} \lor \bar{2})$$

So each of the blocks between the commas or $\land$ are clauses. On the left is a growing list of literals (atoms or their negation). On the right are the rules being applied (like Decide). But I don't understand (a) how the rules are being applied / why they are chosen at the time they are chosen, (b) how it results in an annotated literal for $M$ on the left, and (c) why some of them are marked in bold as the "decision" literals.

The final result, from my understanding, is the model $M$ (on the left) that satisfies the formula $F$ on the right. Essentially, it's a valuation.

Wondering if one could clarify how the first example works, how the annotated literals get added to the model $M$ on the left.