CLIQUE $\leq_p$ SAT

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.

• How would I restrict the formular $v_i \land v_j \implies e_{i, j}$ to be true for at least k variables?

• Is this way in poly-time?

• Is there any better way?

There are many ways to reduce CLIQUE to SAT. Probably the simplest is as follows. Suppose that we have a graph $G = (V,E)$, and interested in a $k$-clique. We will have $k|V|$ variables $x_{iv}$, whose intended meaning is "the $i$th vertex of the clique is $v$". The constraints are:

• There is an $i$th vertex: for all $1 \leq i \leq k$, $\bigvee_{v \in V} x_{iv}$.

• The $i$th and $j$th vertices are different: for all $1 \leq i

• Any two vertices in the clique are connected: for all $1 \leq i

StackExchange Computer Science Q#112715, answer score: 5