Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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?
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}$.
