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?