I read from this question, I have not understood $G$ satisfiable $\implies F$ satisfiable section. In this section case3 is $D$ contains $\bar\ell$.
And author said in the last line "blocked clause (since we haven't used it yet) together with our assumption that $C$ wasn't satisfied by the original assignment $\beta$".
My question is how to use blocked clause definition here? How definition and "$C$ wasn't satisfied by the original assignment $\beta$" use together?
I mean accurately why everything is OK in "case 3" ,yes, using the definition, but please explain how?
We will start from the basic definition and we will use a simple example to support the argument.
Definition: a clause $C$ is blocked by a literal $l \in C$ in a CNF formula $F$ if all binary resolvents of $C$ upon $l$ with clauses from $F \setminus \{ C \}$ are tautologies.
Example: the clause $C = ¬P \lor Q$ is blocked by literal $¬P$ in $F = \{ P \lor ¬Q, ¬Q \lor R \}$ because the only resolvent of $C$ upon $¬P$ is the tautology $Q \lor ¬Q$, obtained by resolving with clause $D = P \lor ¬Q$.
The argument assumes that we have some satisfying assignment $\beta$ for $G = F \setminus \{ C \}$ that does not satisfy $F$ and we want to define a new assignment $\beta'$ that will do.
But $F$ and $G$ only differ in the clause $C$, and thus $β$ does not satisfy $C$, i.e. $\beta(C)= \bot$.
The way to satisfy $C$ is to set one of the literals in $C$ to $\top$, but we know only one literal of $C$: the literal $l$ [$\lnot P$ in our example]. So, we try with $\beta'(l)= \top$ (while keeping all other assignments as in $\beta$) that implies $\beta'(C)=\top$, and we have to check how all other clauses of $F$ are satisfied by $\beta'$.
Then three cases: case 1) neither $l$ nor $\overline l$ are in $D$; it is not affected by the new value for $l$. 2) $l \in D$, an thus $\beta'(l)= \top$ implies $\beta' (D)= \top$.
And now case 3): $\overline l \in D$. But we have that $C$ was blocked by $l$ if $F$ and this means that all binary resolvents of $C$ upon $l$ with clauses from $F \setminus \{ C \}$ are tautologies: thus, the resolvent of $C$ and $D$ must be a tautology, i.e. there must be a literal $k \in D$ such that $\overline k \in C$ [see example above, where $C = \lnot P \lor Q$ and $D = P \lor \lnot Q$].
But we have assumed that for the original assigment $\beta$: $\beta (C)= \bot$ that means that every literal in $C$ must be falsified by $\beta$ and thus also $\beta(\overline k)=\bot$, i.e. $\beta (k)=\top$.
Thus, we have $k \in D$ and $\beta' (k)= \beta(k)= \top$ tha means that $\beta'(D)= \top$.