How to prove that every type can be realized using compactness theorem? I could not understand the proof in David Marker's book because by definition a type $p(x_{1},...,x_{n})$ should be a collection of some formulas(rather than sentences) and I don't know what does "a model $\mathcal{N}_{0}$ that satisfies $p$" mean.
A natural attempt is to "change the variables $x_{i}$ in $p$ to some constant symbols and apply compactness theorem in the extended language", but how do we actually define that? I have just realized that a variable may occur both free and bounded in a formula, like $xEy\land\exists x(xEz)$. It seems that we can avoid such cases by changing variables and get an equivalent formula, but I have never seen this mentioned somewhere.

A set of formulas $\Sigma$ with free variables from $x = (x_1,\dots,x_n)$ is satisfiable if there is a structure $M$ and a tuple $a = (a_1,\dots,a_n)$ from $M$ such that $M\models \varphi(a)$ for every formula $\varphi(x)\in \Sigma$. 
You're right that this is the same as replacing each of the variables $x_i$ with a new constant symbol $c_i$ and asking for the resulting theory to be satisfiable. Of course if you allow variables to occur both free and bound in a formula, you only replace the free instances! This is not hard to formalize.
