[Rule] KSatisfiability to VertexCover

[isPANN]

Source

KSatisfiability (K3, i.e., 3-SAT)

Target

VertexCover (proposed in #986)

Motivation

Classic Garey & Johnson reduction (Theorem 3.3) proving NP-completeness of Vertex Cover from 3-SAT. Establishes the NP-hardness proof chain in the reduction graph. This is the same construction already implemented for 3-SAT → MinimumVertexCover, but targeting the decision version with threshold k = n + 2m.

Reference

Garey & Johnson, Computers and Intractability, 1979, Theorem 3.3.

Reduction Algorithm

Notation:

• Source: 3-SAT instance with n variables x₁, ..., xₙ and m clauses c₁, ..., cₘ, each clause containing exactly 3 literals
• Target: VertexCover instance with graph G = (V, E) and threshold k

Construction:

1. Truth-setting gadgets: For each variable xᵢ (i = 1, ..., n), create two vertices (xᵢ at index 2(i−1) and ¬xᵢ at index 2(i−1)+1) connected by an edge. Total: n edges.
2. Satisfaction-testing gadgets: For each clause cⱼ (j = 1, ..., m), create three vertices at indices 2n+3(j−1), 2n+3(j−1)+1, 2n+3(j−1)+2 forming a triangle. Total: 3m edges.
3. Communication edges: For each literal lₖ (k = 0,1,2) in clause cⱼ, add an edge from the k-th triangle vertex of clause j to the corresponding literal vertex in the truth-setting gadget. If lₖ = xᵢ, connect to vertex 2(i−1); if lₖ = ¬xᵢ, connect to vertex 2(i−1)+1. Total: 3m edges.
4. Set k = n + 2m.

Correctness: The 3-SAT formula is satisfiable if and only if the constructed graph has a vertex cover of size ≤ n + 2m. Each truth-setting edge forces exactly one of {xᵢ, ¬xᵢ} into any minimum cover (contributing n). Each triangle requires at least 2 of 3 vertices (contributing 2m). A satisfying assignment ensures each clause has a true literal whose communication edge is already covered by the truth-setting vertex, so exactly 2 triangle vertices per clause suffice.

Solution extraction: For variable xᵢ, if vertex 2(i−1) (the positive literal) is in the cover, set xᵢ = 1; otherwise set xᵢ = 0.

Size Overhead

Target metric	Formula
num_vertices	2 * num_vars + 3 * num_clauses
num_edges	num_vars + 6 * num_clauses
k	num_vars + 2 * num_clauses

Validation Method

Closed-loop test: construct 3-SAT instance, reduce to VertexCover, solve VertexCover, extract SAT assignment, verify it satisfies the original formula. Also test with an unsatisfiable instance to verify NO.

Example

1. Source instance: 3-SAT with 3 variables, 2 clauses:

   • c₁ = (x₁ ∨ x₂ ∨ x₃)
   • c₂ = (¬x₁ ∨ ¬x₂ ∨ x₃)

2. Construction:

   • Truth-setting vertices: x₁(0), ¬x₁(1), x₂(2), ¬x₂(3), x₃(4), ¬x₃(5)
   • Truth-setting edges: {0,1}, {2,3}, {4,5}
   • Clause 1 triangle: vertices 6,7,8 with edges {6,7}, {7,8}, {6,8}
   • Clause 1 communication: {6,0} (x₁), {7,2} (x₂), {8,4} (x₃)
   • Clause 2 triangle: vertices 9,10,11 with edges {9,10}, {10,11}, {9,11}
   • Clause 2 communication: {9,1} (¬x₁), {10,3} (¬x₂), {11,4} (x₃)
   • k = 3 + 2·2 = 7

3. Target instance: VertexCover with 12 vertices, 15 edges, k = 7.

   • Satisfying assignment: x₁=0, x₂=0, x₃=1
   • Vertex cover: {1, 3, 4, 6, 7, 10, 11}, size = 7 = k → YES

Python validation script

from itertools import combinations, product

num_vars = 3
clauses = [[1, 2, 3], [-1, -2, 3]]
num_clauses = len(clauses)
total_verts = 2 * num_vars + 3 * num_clauses
edges = []

# Truth-setting edges
for i in range(num_vars):
    edges.append((2*i, 2*i+1))

# Clause gadgets + communication edges
for j, clause in enumerate(clauses):
    base = 2 * num_vars + 3 * j
    edges.append((base, base+1))
    edges.append((base+1, base+2))
    edges.append((base, base+2))
    for k_idx, lit in enumerate(clause):
        var_idx = abs(lit) - 1
        lit_vertex = 2 * var_idx if lit > 0 else 2 * var_idx + 1
        edges.append((base + k_idx, lit_vertex))

k = num_vars + 2 * num_clauses
assert total_verts == 12
assert len(edges) == 15
assert k == 7

def is_vertex_cover(verts, edges):
    cover = set(verts)
    return all(u in cover or v in cover for u, v in edges)

# Verify cover {1,3,4,6,7,10,11}
cover = {1, 3, 4, 6, 7, 10, 11}
assert is_vertex_cover(cover, edges)
assert len(cover) == k
print(f"Cover {sorted(cover)} is valid, size {len(cover)} = k={k} ✓")

# Verify minimum VC size = k (SAT ↔ min VC = k)
for size in range(total_verts + 1):
    for combo in combinations(range(total_verts), size):
        if is_vertex_cover(combo, edges):
            assert size == k, f"min VC = {size} != k = {k}"
            print(f"Minimum VC size = {size} = k ✓")
            break
    else:
        continue
    break

# Extract and verify SAT assignment
assignment = []
for i in range(num_vars):
    assignment.append(1 if 2*i in cover else 0)
print(f"Extracted assignment: {assignment}")

for clause in clauses:
    sat = any(
        (lit > 0 and assignment[abs(lit)-1] == 1) or
        (lit < 0 and assignment[abs(lit)-1] == 0)
        for lit in clause
    )
    assert sat, f"Clause {clause} not satisfied"
print("All clauses satisfied ✓")

BibTeX

@book{GareyJohnson1979,
  author    = {Michael R. Garey and David S. Johnson},
  title     = {Computers and Intractability: A Guide to the Theory of NP-Completeness},
  publisher = {W.H. Freeman},
  year      = {1979},
}