CLIQUE $\leq_p$ SAT

Question

i'm trying to reduce CLIQUE to SAT:

• Given: Graph G=(Vertices V, Edges E) and $k \in \mathbb{N}$
• Output: Formular F such that if G contains a complete subgraph of size k, the formular is satisfiable (and vice versa).

I tried doing it the way Cook/Levin showed that SAT is NP-complete by introducing a set of booleans $v_i$ for each vertex and $e_{i, j}$ for an edge going from $v_i$ to $v_j$. Now if $v_i$ is part of the clique, then $e_{i, j}$ must be true iff $v_j$ is also in the clique.

So we can conclude, that $v_i \land v_j \implies e_{i, j}$ and this is for true for at least $i, j \in \{0, ..., k - 1\}$ and $i \neq j$. Also we need to make sure that no edge that doesn't exist can be set to true: $\bigwedge_{(i, j)\notin E} \lnot\, e_{i, j}$.

I don't know if im on the correct way or if I might miss something.

1. How would I restrict the formular $v_i \land v_j \implies e_{i, j}$ to be true for at least k variables?
2. Is this way in poly-time?
3. Is there any better way?