# Reducing k Vertex Cover to SAT (last clause problem)

I am working on a transformation from k Vertex Cover to SAT and I have some issues regarding the last clause in the boolean formula.

Here is my approach: $$\forall \text{ nodes } n_i \in V, \text{ invent variables } v_i$$ $$\forall \text{ edges } (n_i, n_j) \in E, \text{ invent the terms } (v_i \lor v_j) \Rightarrow C_{edges}$$

Is this approach correct or am I missing something?

• Thank you for trying to edit your question to make it more focused. At the same time, editing the question in a way that renders the existing answer inapplicable is less than ideal. It'd be better to make sure the question focuses on the key issue from the start. Anyway, for the answer to this edited question, see cs.stackexchange.com/q/13188/755 and cs.stackexchange.com/a/6522/755. – D.W. Oct 12 '16 at 4:48

First of all, the problem of vertex cover asks whether there is a vertex cover with at most $k$ vertices. Fortunately, there is a vertex cover with at most $k$ vertices iff there is one with exactly $k$ vertices, so your choice of looking for a vertex cover of size exactly $k$ is fine.
Second, you need to describe everything as a CNF, that is, a collection of clauses. You can't just include $$y_{i,j} \equiv (y_{i-1,j} \land \lnot v_i) \lor (y_{i-1,j-1} \land v_i).$$ Fortunately, every formula on $t$ variables can be written as a CNF having at most $2^t$ clauses (exercise), so you can turn this formula into a CNF of constant size.
Finally, you say that you "should write $y_{nk}$ in terms of $v_1 \cdots v_k$", but there is no such requirement. An instance of SAT is just a bunch of clauses. You can use whatever variables and clauses you want; the distinction between original variables $v_i$ and extension variables $y_{i,j}$ is all in your head. If you want to force $y_{n,k}$ to be true, you can just add a singleton clause $y_{n,k}$.