3
$\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
  • 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.
    Commented Oct 12, 2016 at 4:48

1 Answer 1

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$
4
  • 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$ Commented Aug 22, 2016 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$ Commented Aug 22, 2016 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$ Commented Aug 22, 2016 at 15:18
  • $\begingroup$ No, that's your job. Perhaps you should look at examples in textbooks. $\endgroup$ Commented Aug 22, 2016 at 19:08

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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