Blocked Literals
Blocked literals are an optimization of watches. Consider clause $C$, and watches $L_1$ and $L_2$. A blocked literal $B$ is a literal from $C$, where $B$ can also be $L_1$ or $L_2$. When propagating using blocked literals, we do not go through all of $C$. Instead, we only look at $B$. If $B$ is true, then we move on to the following clause.
The pseudocode of propagating with blocked literals looks like this:
propagation(L1)
| for each (B, C) watched by L1
| | if B=true
| | | do nothing
| | else (B=false or B=unassigned) visit clause
| | | if only one unassigned //1
| | | | propagate
| | | end
| | | if all assigned false //2
| | | | conflict
| | | end
| | | if one lit LC of the clause is true //3
| | | | change blocking literal to LC
| | | end
| | | if one literal LC of the clause is unassigned or true //4
| | | | change watched literal L1 to the found literal
| | | end
| | end
| end
end
In the propagation loop, when one literal is true you have the choice between 3 (new!) and 4 (already existing!). You need to have 3, but can also heuristically decide to sometimes use 4.
A good assertion is to make sure that $\text{level}(B) \leq \text{level}(L_1)$.