11.9

Reduction sketch.
For a graph G = (V,E) and target size k:
1. Create boolean variables x[v][i] for every vertex v∈V and every position i∈{1…k}. x[v][i]=1 iff vertex v is placed at the i-th slot of the cover.
2. Encode four groups of clauses:
  a) Each slot is filled: for every i, add clause ∨v x[v][i].
  b) No slot gets two vertices: for all i and pairs v≠u, add ¬x[v][i] ∨ ¬x[u][i].
  c) Vertex occurs once: for each v and i<j, add ¬x[v][i] ∨ ¬x[v][j].
  d) Every edge covered: for each edge (u,v)∈E add clause ∨i (x[u][i] ∨ x[v][i]) (or equivalently one large 2-CNF clause per edge).

Python prototype.
def vc_to_sat(edges, k):
  V = {v for e in edges for v in e}
  idx = { (v,i): n for n,(v,i) in enumerate((v,i) for i in range(k) for v in V) }
  clauses = []
  # a) each position filled
  for i in range(k):
    clauses.append([ idx[(v,i)] for v in V ])
  # b) no two vertices share a slot
  for i in range(k):
    for u in V:
      for v in V:
        if u<v:
          clauses.append([-idx[(u,i)], -idx[(v,i)]])
  # c) vertex appears once
  for v in V:
    for i in range(k):
      for j in range(i+1, k):
        clauses.append([-idx[(v,i)], -idx[(v,j)]])
  # d) every edge covered
  for u,v in edges:
    clause = []
    for i in range(k):
      clause.extend([ idx[(u,i)], idx[(v,i)] ])
    clauses.append(clause)
  return len(idx), clauses

Experiment.
Feeding the generated DIMACS CNF to a modern SAT solver (e.g. MiniSAT or PySAT) solves graphs with ≲30 vertices and small k almost instantly (milliseconds). However, the number of variables is |V|·k and the number of clauses is Θ(k·|V|² + |E|·k), so the encoding explodes for dense graphs or large k. For example, a graph with 100 vertices and k=20 already yields 2000 variables and >200 000 clauses, pushing even industrial solvers.

Practicality verdict.
The reduction is simple to implement and, thanks to powerful SAT engines, works well for small or moderately sized instances. For large, dense, or high-k graphs the quadratic clause blow-up makes it impractical; specialised FPT or approximation algorithms outperform the SAT route there. In short: great as a quick prototype or for modest inputs, but not a universally practical method for computing minimum vertex covers.

Back to Chapter 11