# Reduce Vertex cover to SAT

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?

• Converting from DNF to CNF can give an exponential blow-up in the size of the formula. Unless you can guarantee that this won't happen for the DNFs you need to deal with, your reduction won't run in polynomial time. Commented Mar 9, 2014 at 20:45
• Here you go Amrith citeseerx.ist.psu.edu/viewdoc/… I hope that answers your question
– user15610
Commented Mar 12, 2014 at 17:03

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.