2
$\begingroup$

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?

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – D.W. Oct 12 '16 at 4:48
4
$\begingroup$

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}$.

$\endgroup$
  • 1
    $\begingroup$ You can do whatever you want, as long as the end result is an instance of SAT. Any further limitations are voluntary. $\endgroup$ – Yuval Filmus Aug 22 '16 at 14:55
  • 1
    $\begingroup$ You have to include all the clauses that you mentioned. If you have polynomially many clauses, and it takes polynomial time to generate them, then the entire transformation will be polynomial time. $\endgroup$ – Yuval Filmus Aug 22 '16 at 15:18
  • 1
    $\begingroup$ You don't have to "define" variables. An instance of SAT is a collection of clauses, and every variable which they use is legitimate. $\endgroup$ – Yuval Filmus Aug 22 '16 at 15:18
  • $\begingroup$ No, that's your job. Perhaps you should look at examples in textbooks. $\endgroup$ – Yuval Filmus Aug 22 '16 at 19:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.