Reduce k-Independent Set instance to a CNF SAT instance

Question

given a graph G, we are tasked to verify if it contains a k-sized independent set.

how can I reduce this problem to a SAT clauses ?

Answer 1

To reduce the k-Independent Set problem to a CNF-SAT instance, we first describe the idea in terms of choices rather than symbols. For a given graph, the goal is to determine whether it is possible to select exactly k different vertices such that no two of them are connected by an edge. To encode this as a SAT problem, we imagine that there are k “positions” to be filled, and each position must be assigned exactly one vertex from the graph. A truth assignment will represent which vertex is placed in each position.

First, we add clauses that guarantee every position is filled. For each of the k positions, we include a clause stating that at least one of the graph’s vertices must be chosen for that position. This ensures that all k slots are occupied. Next, we add clauses that guarantee that no position contains more than one vertex. For each position and for every pair of different vertices, we include a clause saying that they cannot both be chosen in the same position. This forces each position to contain exactly one vertex.

Then, we make sure that the same vertex is not used in two different positions. For every vertex and every pair of different positions, we add a clause stating that this vertex cannot appear in both positions at the same time. This ensures that all k chosen vertices are distinct.

Finally, we enforce the independence condition. For every edge in the graph, and for every pair of different positions, we add a clause stating that the two endpoints of the edge cannot both be selected in those positions. In other words, if two vertices are connected by an edge, the formula forbids them from both being chosen as part of the solution. This prevents adjacent vertices from appearing together in the selected set.

With these clauses, any satisfying assignment corresponds to choosing exactly k distinct vertices, one for each position, such that no two chosen vertices are adjacent. Conversely, any independent set of size k in the graph gives a satisfying assignment to the formula. Therefore, the constructed CNF formula is satisfiable if and only if the original graph contains an independent set of size k.