First of all, I assume that $C_1^4 \equiv O \iff (X_2 \lor A)$ in accordance to $F_1$. Second, note that 3CF as defined in the exercise is equivalent to 3CNF. In the following, I will denote with $\phi_X$ the subformula of the given formula $F$ which has been assigned new variable $X$ by the construction. For example, $\phi_A=(\lnot P \land S)$ and $\phi_O = F_1$.
$\renewcommand{\models}{\mathop{|\!\!\!=}}\newcommand{\rmodels}{\mathop{=\!\!\!|}} \newcommand{\semeq}{\models\!\rmodels}$
Satisfaction equivalence
I don't see why $X_1$ is satisfiable
$X_1$ is a single variable and thus trivially satisfiable (by setting it to $1$). The $C_1^i$ essentially take apart $F_1$ operator by operator, introducing new variables that have to evaluate to the same truth values as their respective subformulae. Using $\{O\}$ as clause of $C_1$ guarantees the statement, essentially (as "$O \semeq F_1$", given $C_1$).
Proof
Assume $F_1$ is satisfiable and let $\psi$ be a satisfying valuation of the variables. Construct $\psi'$ by extending $\psi$ with $\psi'(X) = \psi(\phi_{X})$ for $X \in \{X_1,X_2,A,O\}$. As a consequence, $\psi'$ satisfies all $C_i^1$. Because $\psi(F_1)=1$ by assumption, we have chosen $\psi'(O)=1$. Therefore, $\psi'(C_1)=1$.
Conversely, assume $C_1$ is satisfiable and let $\psi$ a satisfying valuation. Clearly, $\psi(O)=1$ and $\psi(C_1^4)=1$. Therefore, $\psi(\psi_O)=1$. Because $\psi_O=F_1$, we are done -- $\psi$ satisfies $F_1$. In order to be rigorous, we would have to iterate this argument top-down, following the structure of $F_1$, to unfold $X_2$ and then $X_1$ (in the general case, we would need a structural induction here).
Size restriction
The constraining formulae all have the same form and are small (three literals, two operators). You can transform those into equivalent 3CF formulae locally, i.e. ignoring the others. This conversion always yields formulae with at most 24 literals, that is at most 8 clauses. This can be shown by dull calculation.
Details
The general form of a contraining formula is $A \iff (A \circ B)$ for $\circ$ some logical operator. Let us transform it into 3CF using laws and rules of boolean algebra.
$\qquad \begin{align}
C^i &\equiv X \iff (A \circ B) \\
&\semeq\ [X \land (A \circ B)] \lor [\lnot X \land \lnot(A \circ B)] \\
&\semeq\ [\lnot X \lor (A \circ B)] \land [ X \lor \lnot(A \circ B)]
\end{align}$
Now, for $\circ = \land$, we use both distributive and associative law resp. De Morgan's rule:
$\qquad \begin{align}
C^i &\semeq\ [\lnot X \lor (A \land B)] \land [ X \lor \lnot(A \land B)] \\
&\semeq\ [\lnot X \lor A] \land [\lnot X \lor B] \land [ X \lor \lnot A \lor \lnot B]
\end{align}$
This has three clauses (after padding with redundant literals, nine literals). For $\circ \in \{\lor, \to\}$¹ this works exactly the same way. You can proceed similarly for other choices of $\circ$, such as $\oplus$ or $\iff$, depending on which operators are allowed in your setting.
Generalisation
This is just a matter of writing down what the example does in general terms. Let $F$ an arbitrary propositional formula, w.l.o.g. without "negation chains"². Now do the following.
$\quad$ Let $i=0$.
$\quad$ Until $F$ is a literal, do
$\qquad$ Increase $i$ by one.
$\qquad$ Pick a subformula of $F$ of the form $L_1 \circ L_2 = \phi$ with $L_1,L_2$ literals.
$\qquad$ Let $C^i \equiv X_i \iff (L_1 \circ L_2)$.
$\qquad$ Replace $\phi$ with $X_i$ in $F$.
$\quad$ For all $j=1,\dots,i$, convert $C^j$ into 3CF by finite case distinction.
$\quad$ Return $[F \lor F \lor F] \land \bigwedge_{j=1}^{i} C^j$.
Note that $F = X_i$ after the loop. For intuition and implementation purposes, think of a formula as a tree: operators are inner nodes, leaves are literals. Above algorithm iteratively contracts subtrees of height two into leaves, collecting the $C^j$ as "mapping" from new variable to the removed subtree along the way.
- Remember $A \to B \semeq \lnot A \lor B$.
- We can always use $\lnot \lnot A \semeq A$.
