Problem Detail: I need to reduce the vertex cover problem to a SAT problem, or rather tell whether a vertex cover of size k exists for a given graph, after solving with a SAT solver. I know how to reduce a 3-SAT problem to vertex cover problem, by constructing the subgraphs for each variable (x, !x) and for each clause (a triable). But I am not getting,how to do other way round? I was thinking of first forming a DNF ,with electing k vertices at first and then convert it to a CNF, by enumerating all clauses. Is there any other method?
Asked By : Amrith Krishna
Answered By : Niklas B.
Let’s introduce a variable $x_i$ for every node $i$, representing the condition that the node is part of the vertex cover. Then for every edge ${v,w}$ we introduce the clause $x_v lor x_w$. We have the additional condition $x_1 + x_2 + ldots + x_n leq k$. We can combine an addition circuit to compute the bits of the sum with a comparator circuit to enforce the inequality. The CNF of the resulting circuit has only polynomially many clauses.
Best Answer from StackOverflow
Question Source : http://cs.stackexchange.com/questions/22426
