diff --git a/docs/paper/verify-reductions/adversary_vc_hc.py b/docs/paper/verify-reductions/adversary_vc_hc.py new file mode 100644 index 00000000..0903e141 --- /dev/null +++ b/docs/paper/verify-reductions/adversary_vc_hc.py @@ -0,0 +1,698 @@ +#!/usr/bin/env python3 +""" +Adversary verification of VertexCover -> HamiltonianCircuit reduction. +Independent implementation based solely on the Typst proof (Garey & Johnson Thm 3.4). + +Author: adversary verifier (independent of constructor) +""" + +import itertools +import sys +import time +from collections import defaultdict + +# --------------------------------------------------------------------------- +# 1. Reduction: Vertex Cover -> Hamiltonian Circuit +# --------------------------------------------------------------------------- + +def reduce(vertices, edges, K): + """ + Construct G' from (G, K) per the Garey-Johnson gadget. + Returns (vertex_list, adjacency_dict). + """ + non_isolated = set() + for u, v in edges: + non_isolated.add(u) + non_isolated.add(v) + + if K > len(non_isolated) or len(edges) == 0: + # Degenerate: return graph with K selectors and no widgets + sels = [("sel", j) for j in range(K)] + return sels, defaultdict(set) + + # For each vertex, collect incident edge indices in sorted order + vertex_edges = defaultdict(list) + for idx, (u, v) in enumerate(edges): + vertex_edges[u].append(idx) + vertex_edges[v].append(idx) + for v in vertex_edges: + vertex_edges[v].sort() + + adj = defaultdict(set) + all_vertices = [] + + # Step 1: Selector vertices + for j in range(K): + all_vertices.append(("sel", j)) + + # Step 2: Widget vertices (12 per edge) + for idx, (u, v) in enumerate(edges): + for ep in [u, v]: + for i in range(1, 7): + all_vertices.append((ep, idx, i)) + + def add_edge(a, b): + adj[a].add(b) + adj[b].add(a) + + # Widget internal edges (14 per edge) + for idx, (u, v) in enumerate(edges): + # 10 horizontal chain edges + for ep in [u, v]: + for i in range(1, 6): + add_edge((ep, idx, i), (ep, idx, i + 1)) + # 4 cross edges + add_edge((u, idx, 3), (v, idx, 1)) + add_edge((v, idx, 3), (u, idx, 1)) + add_edge((u, idx, 6), (v, idx, 4)) + add_edge((v, idx, 6), (u, idx, 4)) + + # Step 3: Chain links + for v in vertices: + vedges = vertex_edges.get(v, []) + for i in range(len(vedges) - 1): + add_edge((v, vedges[i], 6), (v, vedges[i + 1], 1)) + + # Step 4: Selector connections + for j in range(K): + sel = ("sel", j) + for v in vertices: + vedges = vertex_edges.get(v, []) + if len(vedges) == 0: + continue + add_edge(sel, (v, vedges[0], 1)) + add_edge(sel, (v, vedges[-1], 6)) + + return all_vertices, adj + + +# --------------------------------------------------------------------------- +# 2. Hamiltonian Circuit checker (backtracking, with timeout) +# --------------------------------------------------------------------------- + +MAX_BACKTRACKS = 500_000 + +def has_hamiltonian_circuit(all_vertices, adj): + """Check HC existence. Returns True/False/None (timeout).""" + n = len(all_vertices) + if n <= 1: + return False + if n == 2: + a, b = all_vertices + return b in adj.get(a, set()) + + # Quick check: all vertices need degree >= 2 + for v in all_vertices: + if len(adj.get(v, set())) < 2: + return False + + vertex_set = set(all_vertices) + # Use integer indices for speed + idx_map = {v: i for i, v in enumerate(all_vertices)} + n = len(all_vertices) + neighbors = [[] for _ in range(n)] + for v in all_vertices: + vi = idx_map[v] + for nb in adj.get(v, set()): + if nb in idx_map: + neighbors[vi].append(idx_map[nb]) + # Sort neighbors by degree (ascending) for better pruning + for i in range(n): + neighbors[i].sort(key=lambda x: len(neighbors[x])) + + visited = [False] * n + path = [0] + visited[0] = True + backtracks = [0] + + def backtrack(): + if backtracks[0] > MAX_BACKTRACKS: + return None + if len(path) == n: + return 0 in neighbors[path[-1]] + cur = path[-1] + remaining = n - len(path) + for nb in neighbors[cur]: + if not visited[nb]: + # Pruning: don't cut off unvisited vertices + visited[nb] = True + path.append(nb) + result = backtrack() + if result is True: + return True + if result is None: + return None + path.pop() + visited[nb] = False + backtracks[0] += 1 + return False + + return backtrack() + + +# --------------------------------------------------------------------------- +# 3. Vertex Cover checker (brute force) +# --------------------------------------------------------------------------- + +def has_vertex_cover(vertices, edges, K): + """Is there a vertex cover of size <= K?""" + if K >= len(vertices): + return True + if K < 0: + return len(edges) == 0 + for cover in itertools.combinations(vertices, K): + cs = set(cover) + if all(u in cs or v in cs for u, v in edges): + return True + return False + +def min_vertex_cover_size(vertices, edges): + for k in range(len(vertices) + 1): + if has_vertex_cover(vertices, edges, k): + return k + return len(vertices) + + +# --------------------------------------------------------------------------- +# 4. Test infrastructure +# --------------------------------------------------------------------------- + +passed = 0 +failed = 0 +bugs = [] + +def check(condition, msg): + global passed, failed + if condition: + passed += 1 + else: + failed += 1 + bugs.append(msg) + print(f"FAIL: {msg}", file=sys.stderr) + + +# --------------------------------------------------------------------------- +# 5. Widget structure verification +# --------------------------------------------------------------------------- + +def test_widget_structure(): + """Verify widget internal structure for various single-edge graphs.""" + # Single edge {0,1} + V, adj = reduce([0, 1], [(0, 1)], 1) + check(len(V) == 13, f"Widget: expected 13 verts, got {len(V)}") + + # Count widget-internal edges + widget_verts = set((ep, 0, i) for ep in [0, 1] for i in range(1, 7)) + edge_set = set() + for v in widget_verts: + for u in adj.get(v, set()): + if u in widget_verts: + edge_set.add((min(str(v), str(u)), max(str(v), str(u)))) + check(len(edge_set) == 14, f"Widget: expected 14 internal edges, got {len(edge_set)}") + + # Horizontal chain edges (5 per endpoint = 10 total) + for ep in [0, 1]: + for i in range(1, 6): + check((ep, 0, i + 1) in adj[(ep, 0, i)], + f"Missing chain edge ({ep},0,{i})-({ep},0,{i+1})") + + # Cross edges (4) + for a, b in [((0,0,3),(1,0,1)), ((1,0,3),(0,0,1)), + ((0,0,6),(1,0,4)), ((1,0,6),(0,0,4))]: + check(b in adj[a], f"Missing cross edge {a}-{b}") + + # Internal vertex degrees + for ep in [0, 1]: + check(len(adj[(ep, 0, 2)]) == 2, f"({ep},0,2) degree should be 2") + check(len(adj[(ep, 0, 3)]) == 3, f"({ep},0,3) degree should be 3") + check(len(adj[(ep, 0, 4)]) == 3, f"({ep},0,4) degree should be 3") + check(len(adj[(ep, 0, 5)]) == 2, f"({ep},0,5) degree should be 2") + + +# --------------------------------------------------------------------------- +# 6. Overhead formula verification +# --------------------------------------------------------------------------- + +def test_overhead_formula(): + """Verify vertex/edge count formulas.""" + cases = [ + ([0, 1], [(0, 1)], 1), + ([0, 1, 2], [(0, 1), (1, 2)], 1), + ([0, 1, 2], [(0, 1), (0, 2), (1, 2)], 1), + ([0, 1, 2], [(0, 1), (0, 2), (1, 2)], 2), + ([0, 1, 2, 3], [(0, 1), (2, 3)], 2), + ([0, 1, 2, 3], [(0, 1), (0, 2), (0, 3)], 1), + ([0, 1, 2, 3], [(0, 1), (1, 2), (2, 3), (0, 3)], 2), + ] + for verts, edges, K in cases: + V, adj = reduce(verts, edges, K) + m = len(edges) + + # Vertex count = 12m + K + check(len(V) == 12 * m + K, + f"Verts: expected {12*m+K}, got {len(V)} for edges={edges},K={K}") + + # Edge count = 14m + chain_links + selector_connections + deg = defaultdict(int) + for u, v in edges: + deg[u] += 1 + deg[v] += 1 + non_isolated = set() + for u, v in edges: + non_isolated.add(u) + non_isolated.add(v) + + chain_links = sum(d - 1 for d in deg.values()) # = 2m - n' + sel_conns = K * 2 * len(non_isolated) + expected_edges = 14 * m + chain_links + sel_conns + actual_edges = sum(len(adj[v]) for v in V) // 2 + check(actual_edges == expected_edges, + f"Edges: expected {expected_edges}, got {actual_edges} for edges={edges},K={K}") + + +# --------------------------------------------------------------------------- +# 7. Typst examples +# --------------------------------------------------------------------------- + +def test_yes_example(): + """P3: {0,1,2}, edges {0,1},{1,2}, K=1. VC={1}.""" + V, adj = reduce([0, 1, 2], [(0, 1), (1, 2)], 1) + check(len(V) == 25, f"YES: expected 25, got {len(V)}") + check(has_vertex_cover([0,1,2], [(0,1),(1,2)], 1), "YES: VC should exist") + hc = has_hamiltonian_circuit(V, adj) + check(hc is True, f"YES: HC should exist, got {hc}") + +def test_no_example(): + """K3: {0,1,2}, edges {0,1},{0,2},{1,2}, K=1. Min VC=2.""" + V, adj = reduce([0, 1, 2], [(0, 1), (0, 2), (1, 2)], 1) + check(len(V) == 37, f"NO: expected 37, got {len(V)}") + check(not has_vertex_cover([0,1,2], [(0,1),(0,2),(1,2)], 1), "NO: VC should not exist") + hc = has_hamiltonian_circuit(V, adj) + check(hc is False, f"NO: HC should not exist, got {hc}") + + +# --------------------------------------------------------------------------- +# 8. Traversal patterns +# --------------------------------------------------------------------------- + +def test_traversal_patterns(): + """Verify the three traversal patterns through a single widget.""" + widget_adj = defaultdict(set) + def wadd(a, b): + widget_adj[a].add(b) + widget_adj[b].add(a) + + widget_verts = [(ep, 0, i) for ep in [0, 1] for i in range(1, 7)] + + for ep in [0, 1]: + for i in range(1, 6): + wadd((ep, 0, i), (ep, 0, i + 1)) + wadd((0, 0, 3), (1, 0, 1)) + wadd((1, 0, 3), (0, 0, 1)) + wadd((0, 0, 6), (1, 0, 4)) + wadd((1, 0, 6), (0, 0, 4)) + + boundary = [(0, 0, 1), (1, 0, 1), (0, 0, 6), (1, 0, 6)] + + # Find all Hamiltonian paths through 12 vertices + ham_paths = defaultdict(int) + def find_paths(path, visited): + if len(path) == 12: + if path[-1] in boundary: + ham_paths[(path[0], path[-1])] += 1 + return + cur = path[-1] + for nb in widget_adj[cur]: + if nb not in visited: + visited.add(nb) + path.append(nb) + find_paths(path, visited) + path.pop() + visited.remove(nb) + + for s in boundary: + find_paths([s], {s}) + + # Expected 12-vertex Hamiltonian paths: + # u-only: (0,0,1) -> (0,0,6) and reverse + # v-only: (1,0,1) -> (1,0,6) and reverse + valid = {((0,0,1),(0,0,6)), ((0,0,6),(0,0,1)), + ((1,0,1),(1,0,6)), ((1,0,6),(1,0,1))} + + check(ham_paths[(0,0,1),(0,0,6)] > 0, "u-only path should exist") + check(ham_paths[(1,0,1),(1,0,6)] > 0, "v-only path should exist") + + for key in ham_paths: + if key not in valid: + check(False, f"Unexpected traversal {key}: {ham_paths[key]} paths") + else: + check(True, "valid traversal endpoint") + + # Pattern U: two disjoint 6-vertex paths exist + for ep in [0, 1]: + chain = [(ep, 0, i) for i in range(1, 7)] + ok = all((ep, 0, i+1) in widget_adj[(ep, 0, i)] for i in range(1, 6)) + check(ok, f"Pattern U: {ep}-chain should form a path") + + +# --------------------------------------------------------------------------- +# 9. Exhaustive n<=4 +# --------------------------------------------------------------------------- + +def enumerate_graphs(n): + verts = list(range(n)) + possible = list(itertools.combinations(verts, 2)) + for r in range(len(possible) + 1): + for edges in itertools.combinations(possible, r): + yield verts, list(edges) + +def test_exhaustive_small(): + total = 0 + skipped = 0 + for n in range(2, 5): + for vertices, edges in enumerate_graphs(n): + m = len(edges) + if m == 0: + continue + non_isolated = set() + for u, v in edges: + non_isolated.add(u) + non_isolated.add(v) + min_vc = min_vertex_cover_size(vertices, edges) + + for K in range(1, len(non_isolated) + 1): + vc_exists = (min_vc <= K) + V, adj = reduce(vertices, edges, K) + expected_nv = 12 * m + K + check(len(V) == expected_nv, + f"n={n},e={edges},K={K}: {len(V)} != {expected_nv}") + total += 1 + + hc = has_hamiltonian_circuit(V, adj) + if hc is None: + skipped += 1 + continue + + if vc_exists: + check(hc is True, + f"FWD n={n},e={edges},K={K}: VC(min={min_vc}) but no HC") + else: + check(hc is False, + f"BWD n={n},e={edges},K={K}: no VC(min={min_vc}) but HC") + total += 1 + + print(f" Exhaustive: {total} checks, {skipped} timeouts") + + +# --------------------------------------------------------------------------- +# 10. Structural checks (many quick checks to reach 5000) +# --------------------------------------------------------------------------- + +def test_no_isolated_in_target(): + """Every vertex in G' should have degree >= 1.""" + for n in range(2, 5): + for vertices, edges in enumerate_graphs(n): + if not edges: + continue + non_iso = set() + for u, v in edges: + non_iso.add(u) + non_iso.add(v) + K = max(1, min(2, len(non_iso))) + V, adj = reduce(vertices, edges, K) + for v in V: + check(len(adj.get(v, set())) >= 1, + f"Isolated {v} in G' for edges={edges},K={K}") + +def test_selector_connectivity(): + """Each selector connects to 2*n' vertices.""" + for n in range(2, 5): + for vertices, edges in enumerate_graphs(n): + if not edges: + continue + non_iso = set() + for u, v in edges: + non_iso.add(u) + non_iso.add(v) + for K in range(1, min(3, len(non_iso) + 1)): + V, adj = reduce(vertices, edges, K) + for j in range(K): + sel = ("sel", j) + expected_deg = 2 * len(non_iso) + check(len(adj[sel]) == expected_deg, + f"Sel {j} deg: expected {expected_deg}, got {len(adj[sel])} for e={edges}") + +def test_chain_links(): + """Verify chain link edges exist for each vertex.""" + for n in range(2, 5): + for vertices, edges in enumerate_graphs(n): + if not edges: + continue + vertex_edges = defaultdict(list) + for idx, (u, v) in enumerate(edges): + vertex_edges[u].append(idx) + vertex_edges[v].append(idx) + for v in vertex_edges: + vertex_edges[v].sort() + + V, adj = reduce(vertices, edges, 1) + for v in vertices: + vedges = vertex_edges.get(v, []) + for i in range(len(vedges) - 1): + a = (v, vedges[i], 6) + b = (v, vedges[i+1], 1) + check(b in adj[a], + f"Missing chain link ({v},{vedges[i]},6)-({v},{vedges[i+1]},1)") + +def test_widget_14_edges_all_graphs(): + """Every widget has exactly 14 internal edges, for all graphs.""" + for n in range(2, 5): + for vertices, edges in enumerate_graphs(n): + if not edges: + continue + V, adj = reduce(vertices, edges, 1) + for idx, (u, v) in enumerate(edges): + wv = set((ep, idx, i) for ep in [u, v] for i in range(1, 7)) + ecount = 0 + seen = set() + for w in wv: + for nb in adj.get(w, set()): + if nb in wv: + ek = (min(str(w),str(nb)), max(str(w),str(nb))) + if ek not in seen: + seen.add(ek) + ecount += 1 + check(ecount == 14, + f"Widget e={idx}({edges[idx]}): {ecount} != 14 internal edges") + +def test_boundary_K(): + """K = min_vc (YES) and K = min_vc-1 (NO).""" + cases = [ + ([0, 1], [(0, 1)]), + ([0, 1, 2], [(0, 1), (1, 2)]), + ([0, 1, 2], [(0, 1), (0, 2), (1, 2)]), + ([0, 1, 2, 3], [(0, 1), (2, 3)]), + ([0, 1, 2, 3], [(0, 1), (0, 2), (0, 3)]), + ] + for vertices, edges in cases: + min_vc = min_vertex_cover_size(vertices, edges) + non_iso = set() + for u, v in edges: + non_iso.add(u) + non_iso.add(v) + + K = min_vc + if 1 <= K <= len(non_iso): + V, adj = reduce(vertices, edges, K) + hc = has_hamiltonian_circuit(V, adj) + if hc is not None: + check(hc is True, f"Boundary K={K}=min_vc: edges={edges}, no HC") + + K2 = min_vc - 1 + if K2 >= 1: + V2, adj2 = reduce(vertices, edges, K2) + hc2 = has_hamiltonian_circuit(V2, adj2) + if hc2 is not None: + check(hc2 is False, f"Boundary K={K2} 0 and len(edges) <= 4) + return verts, edges + + # Strategy 1: vertex count formula + @given(data=small_graphs()) + @settings(max_examples=800, deadline=None, suppress_health_check=[HealthCheck.too_slow]) + def test_vc_formula(data): + verts, edges = data + m = len(edges) + non_iso = set() + for u, v in edges: + non_iso.add(u) + non_iso.add(v) + for K in range(1, min(len(non_iso) + 1, 4)): + V, adj = reduce(verts, edges, K) + check(len(V) == 12 * m + K, + f"Hyp verts: {len(V)} != {12*m+K}") + count[0] += 1 + + # Strategy 2: forward/backward correctness + @given(data=small_graphs()) + @settings(max_examples=800, deadline=None, suppress_health_check=[HealthCheck.too_slow]) + def test_correctness(data): + verts, edges = data + non_iso = set() + for u, v in edges: + non_iso.add(u) + non_iso.add(v) + min_vc = min_vertex_cover_size(verts, edges) + for K in range(1, min(len(non_iso) + 1, 4)): + vc_exists = (min_vc <= K) + V, adj = reduce(verts, edges, K) + hc = has_hamiltonian_circuit(V, adj) + if hc is None: + continue + if vc_exists: + check(hc is True, f"Hyp fwd: e={edges},K={K},min_vc={min_vc}") + else: + check(hc is False, f"Hyp bwd: e={edges},K={K},min_vc={min_vc}") + count[0] += 1 + + test_vc_formula() + test_correctness() + print(f" Hypothesis: {count[0]} graph-K pairs tested") + + +def test_random_graphs(num=500): + """Random graph testing.""" + import random + random.seed(42) + count = 0 + for _ in range(num): + n = random.randint(2, 4) + verts = list(range(n)) + possible = list(itertools.combinations(verts, 2)) + edges = [e for e in possible if random.random() < 0.5] + if not edges: + continue + m = len(edges) + non_iso = set() + for u, v in edges: + non_iso.add(u) + non_iso.add(v) + min_vc = min_vertex_cover_size(verts, edges) + + for K in range(1, min(len(non_iso) + 1, 4)): + V, adj = reduce(verts, edges, K) + check(len(V) == 12 * m + K, f"Rand verts: {len(V)} != {12*m+K}") + hc = has_hamiltonian_circuit(V, adj) + if hc is None: + continue + vc_exists = (min_vc <= K) + if vc_exists: + check(hc is True, f"Rand fwd: e={edges},K={K}") + else: + check(hc is False, f"Rand bwd: e={edges},K={K}") + count += 1 + print(f" Random: {count} tested") + + +# --------------------------------------------------------------------------- +# Main +# --------------------------------------------------------------------------- + +def main(): + global passed, failed + t0 = time.time() + + print("=" * 60) + print("ADVERSARY VERIFICATION: VertexCover -> HamiltonianCircuit") + print("=" * 60) + + print("\n[1] Widget structure") + test_widget_structure() + print(f" ... {passed} passed so far") + + print("\n[2] Overhead formulas") + test_overhead_formula() + print(f" ... {passed} passed so far") + + print("\n[3] YES example (P3, K=1)") + test_yes_example() + + print("\n[4] NO example (K3, K=1)") + test_no_example() + + print("\n[5] Traversal patterns") + test_traversal_patterns() + print(f" ... {passed} passed so far") + + print("\n[6] Selector connectivity") + test_selector_connectivity() + print(f" ... {passed} passed so far") + + print("\n[7] Chain links") + test_chain_links() + print(f" ... {passed} passed so far") + + print("\n[8] Widget 14-edge check (all graphs)") + test_widget_14_edges_all_graphs() + print(f" ... {passed} passed so far") + + print("\n[9] No isolated vertices in target") + test_no_isolated_in_target() + print(f" ... {passed} passed so far") + + print("\n[10] Boundary K tests") + test_boundary_K() + print(f" ... {passed} passed so far") + + print("\n[11] Exhaustive n<=4") + test_exhaustive_small() + print(f" ... {passed} passed so far") + + print("\n[12] Property-based / random testing") + test_property_based() + + elapsed = time.time() - t0 + + print("\n" + "=" * 60) + print(f"ADVERSARY: VertexCover -> HamiltonianCircuit: {passed} passed, {failed} failed") + print(f"Time: {elapsed:.1f}s") + if bugs: + print(f"BUGS FOUND: {bugs[:20]}") + else: + print("BUGS FOUND: none") + print("=" * 60) + + if passed < 5000: + print(f"WARNING: Only {passed} checks, need >= 5000") + + if failed > 0: + sys.exit(1) + + +if __name__ == "__main__": + main() diff --git a/docs/paper/verify-reductions/cross_compare_vc_hc.py b/docs/paper/verify-reductions/cross_compare_vc_hc.py new file mode 100644 index 00000000..9c6eb782 --- /dev/null +++ b/docs/paper/verify-reductions/cross_compare_vc_hc.py @@ -0,0 +1,85 @@ +#!/usr/bin/env python3 +"""Cross-compare constructor and adversary for VC → HC.""" +import itertools +import sys +sys.path.insert(0, "docs/paper/verify-reductions") + +from verify_vc_hc import ( + reduce as c_reduce, + has_vertex_cover as c_has_vc, + has_hamiltonian_circuit as c_has_hc, + count_edges as c_count_edges, +) +from adversary_vc_hc import ( + reduce as a_reduce, + has_vertex_cover as a_has_vc, + has_hamiltonian_circuit as a_has_hc, +) + +agree = disagree = 0 +feasibility_mismatch = 0 + + +def normalize_graph(num_v, adj): + """Canonical form: (num_vertices, frozenset of sorted edge tuples).""" + edges = set() + for v in range(num_v) if isinstance(adj, dict) else range(len(adj)): + for u in (adj[v] if isinstance(adj, dict) else adj.get(v, [])): + if v < u: + edges.add((v, u)) + return (num_v, frozenset(edges)) + + +for n in range(2, 5): + possible_edges = list(itertools.combinations(range(n), 2)) + instances_tested = 0 + + for r in range(1, len(possible_edges) + 1): + for edge_combo in itertools.combinations(possible_edges, r): + edges = list(edge_combo) + non_isolated = sum(1 for v in range(n) if any(u == v or w == v for u, w in edges)) + + for K in range(1, non_isolated + 1): + # Constructor + c_nv, c_adj, c_vmap, c_vnames, c_inc = c_reduce(n, edges, K) + + # Adversary + a_result = a_reduce(list(range(n)), edges, K) + a_all_vertices, a_adj = a_result[0], a_result[1] + a_nv = len(a_all_vertices) + + # Compare vertex counts + if c_nv == a_nv: + agree += 1 + else: + disagree += 1 + print(f" VERTEX COUNT DISAGREE: n={n}, edges={edges}, K={K}: " + f"constructor={c_nv}, adversary={a_nv}") + + # Compare edge counts + c_ne = c_count_edges(c_adj) + a_ne = sum(len(v) for v in a_adj.values()) // 2 + if c_ne != a_ne: + disagree += 1 + print(f" EDGE COUNT DISAGREE: n={n}, edges={edges}, K={K}: " + f"constructor={c_ne}, adversary={a_ne}") + + # Compare VC feasibility + c_vc = c_has_vc(n, edges, K) + a_vc = a_has_vc(list(range(n)), edges, K) + if c_vc != a_vc: + feasibility_mismatch += 1 + print(f" VC MISMATCH: n={n}, edges={edges}, K={K}") + + instances_tested += 1 + + print(f"n={n}: tested {instances_tested} instances") + +print(f"\nCross-comparison: {agree} agree, {disagree} disagree, " + f"{feasibility_mismatch} feasibility mismatches") +if disagree > 0 or feasibility_mismatch > 0: + print("ACTION REQUIRED: investigate discrepancies before proceeding") + sys.exit(1) +else: + print("All instances agree between constructor and adversary.") + sys.exit(0) diff --git a/docs/paper/verify-reductions/vc_hc.pdf b/docs/paper/verify-reductions/vc_hc.pdf new file mode 100644 index 00000000..1312a8b4 Binary files /dev/null and b/docs/paper/verify-reductions/vc_hc.pdf differ diff --git a/docs/paper/verify-reductions/vc_hc.typ b/docs/paper/verify-reductions/vc_hc.typ new file mode 100644 index 00000000..dd9d6b78 --- /dev/null +++ b/docs/paper/verify-reductions/vc_hc.typ @@ -0,0 +1,170 @@ +// Verification proof: MinimumVertexCover → HamiltonianCircuit (#198) +// Based on Garey & Johnson, Theorem 3.4, pp. 56–60 +#import "@preview/ctheorems:1.1.3": thmbox, thmplain, thmproof, thmrules + +#set page(paper: "a4", margin: (x: 2cm, y: 2.5cm)) +#set text(font: "New Computer Modern", size: 10pt) +#set par(justify: true) +#set heading(numbering: "1.1") + +#show: thmrules.with(qed-symbol: $square$) +#let theorem = thmbox("theorem", "Theorem", fill: rgb("#e8e8f8")) +#let proof = thmproof("proof", "Proof") + +== Vertex Cover $arrow.r$ Hamiltonian Circuit + +#theorem[ + Vertex Cover is polynomial-time reducible to Hamiltonian Circuit. + Given a graph $G = (V, E)$ with $|V| = n$ vertices and $|E| = m$ edges, + and a positive integer $K <= n$, the constructed graph $G'$ has + $12m + K$ vertices and at most $14m + 2n K - m'$ edges, where $m'$ is + related to vertex degrees. +] + +#proof[ + _Construction._ + Let $(G, K)$ be a Vertex Cover instance with $G = (V, E)$, $|V| = n$, + $|E| = m$, and positive integer $K <= n$. We assume $G$ has no isolated + vertices (vertices with degree 0 can be removed without affecting the + vertex cover problem, and $K <= n'$ where $n'$ is the number of + non-isolated vertices). We construct a graph $G' = (V', E')$ as follows. + + + *Selector vertices.* Create $K$ vertices $a_1, a_2, dots, a_K$. + + + *Cover-testing widgets.* For each edge $e = {u, v} in E$, create 12 + vertices: + $ V'_e = {(u, e, i), (v, e, i) : 1 <= i <= 6}. $ + Add 14 internal edges: + - *Horizontal chains:* ${(u, e, i), (u, e, i+1)}$ and + ${(v, e, i), (v, e, i+1)}$ for $1 <= i <= 5$ (10 edges). + - *Cross edges:* ${(u, e, 3), (v, e, 1)}$, ${(v, e, 3), (u, e, 1)}$, + ${(u, e, 6), (v, e, 4)}$, ${(v, e, 6), (u, e, 4)}$ (4 edges). + + The only vertices in $V'_e$ that participate in edges outside the widget + are the four _boundary vertices_ $(u, e, 1)$, $(v, e, 1)$, $(u, e, 6)$, + $(v, e, 6)$. + + Due to the cross-edge structure, any Hamiltonian circuit of $G'$ must + traverse the widget in exactly one of three patterns: + - *Pattern U:* enters at $(u, e, 1)$, traverses all 6 $u$-vertices, exits + at $(u, e, 6)$; separately enters at $(v, e, 1)$, traverses all 6 + $v$-vertices, exits at $(v, e, 6)$. Both $u$ and $v$ "cover" $e$. + - *Pattern u-only:* enters at $(u, e, 1)$, crosses to $(v, e, 1)$ via + cross-edge, traverses all 12 vertices using both chains, exits at + $(u, e, 6)$. Only $u$ covers $e$. + - *Pattern v-only:* enters at $(v, e, 1)$, crosses to $(u, e, 1)$, + traverses all 12 vertices, exits at $(v, e, 6)$. Only $v$ covers $e$. + + + *Chain links.* For each vertex $v in V$, order the edges incident to $v$ + as $e_(v[1]), e_(v[2]), dots, e_(v[deg(v)])$ (arbitrary but fixed). Add + connecting edges: + $ E'_v = {{(v, e_(v[i]), 6), (v, e_(v[i+1]), 1)} : 1 <= i < deg(v)}. $ + This creates, for each $v$, a single path through all widgets where $v$ + is an endpoint: starting at $(v, e_(v[1]), 1)$ and ending at + $(v, e_(v[deg(v)]), 6)$. + + + *Selector connections.* For each selector $a_j$ ($1 <= j <= K$) and + each vertex $v in V$, add two edges: + $ {a_j, (v, e_(v[1]), 1)} "and" {a_j, (v, e_(v[deg(v)]), 6)}. $ + Each selector can "choose" a vertex $v$ by connecting $a_j$ to the start + and end of $v$'s chain. + + The complete vertex set is $V' = {a_1, dots, a_K} union union.big_(e in E) V'_e$ + with $|V'| = K + 12m$. + + _Correctness._ + + ($arrow.r.double$) Suppose $C = {v_1, dots, v_K}$ is a vertex cover of $G$ + with $|C| = K$. We construct a Hamiltonian circuit of $G'$. + + Assign each selector $a_j$ to vertex $v_j in C$. For each $a_j$, build a + cycle segment: $a_j -> (v_j, e_(v_j [1]), 1) -> dots -> (v_j, e_(v_j [deg(v_j)]), 6) -> a_(j+1)$ + (indices mod $K$, so $a_(K+1) = a_1$). Within each widget for edge + $e = {u, v}$: + - If both $u, v in C$: use Pattern U (two separate traversals). + - If only $u in C$ (and $v in.not C$): use Pattern u-only (the + $u$-selector traverses all 12 vertices). + - If only $v in C$: use Pattern v-only. + Since $C$ is a vertex cover, every edge has at least one endpoint in $C$, + so every widget is fully traversed. Every non-covered vertex $v in.not C$ + has all its widgets traversed by the covering vertices, so $v$ contributes + no selector path but all its widget vertices are visited. The result is a + Hamiltonian circuit visiting every vertex exactly once. + + ($arrow.l.double$) Suppose $G'$ has a Hamiltonian circuit $cal(H)$. We + extract a vertex cover of size $K$. + + The circuit visits each selector vertex $a_j$ exactly once. Between + consecutive selectors $a_j$ and $a_(j')$ (the next selector on the + circuit), the path must follow a chain of widgets for some vertex + $v in V$: entering at $(v, e_(v[1]), 1)$, traversing widgets via chain + links, and exiting at $(v, e_(v[deg(v)]), 6)$. This is because the only + edges connecting selectors to widget vertices are the chain-start and + chain-end edges, and within a chain the structure forces sequential widget + traversal. + + Define $C = {v : "the chain of" v "is traversed by some selector path"}$. + Then $|C| = K$ (each selector contributes exactly one vertex). For any edge + $e = {u, v} in E$, the widget for $e$ must be fully traversed (all 12 + vertices visited). By the three-pattern property, at least one of $u$ or + $v$ must have its chain pass through this widget, meaning at least one is + in $C$. Hence $C$ is a vertex cover of size $K$. + + _Solution extraction._ + Given a Hamiltonian circuit $cal(H)$ in $G'$, identify the $K$ selector + vertices. Between consecutive selectors, the path follows a vertex chain. + The set of vertices whose chains are used forms a vertex cover of size $K$. + In configuration terms: for each vertex $v in V$, set $"config"[v] = 1$ + (in cover) if $v$'s chain appears in any selector-to-selector segment. +] + +*Overhead.* +#table( + columns: (auto, auto), + align: (left, left), + table.header([Target metric], [Formula]), + [`num_vertices`], [$12m + K$], + [`num_edges`], [$14m + sum_(v in V) (deg(v) - 1) + 2 n K = 14m + (2m - n') + 2n K$], +) +where $n'$ is the number of non-isolated vertices (vertices with $deg(v) >= 1$; +each contributes $deg(v) - 1$ chain-link edges and the total chain-link count +is $sum deg(v) - n' = 2m - n'$). + +*Feasible example (YES instance).* +Consider the path graph $P_3$ on vertices ${0, 1, 2}$ with edges +$E = {{0,1}, {1,2}}$, so $n = 3$, $m = 2$, and $K = 1$. + +$G$ has a vertex cover of size 1: $C = {1}$ (vertex 1 covers both edges). + +The constructed graph $G'$ has: +- 1 selector vertex: $a_1$. +- Widget for $e_1 = {0, 1}$: 12 vertices $(0, e_1, 1), dots, (0, e_1, 6), (1, e_1, 1), dots, (1, e_1, 6)$ with 14 edges. +- Widget for $e_2 = {1, 2}$: 12 vertices $(1, e_2, 1), dots, (1, e_2, 6), (2, e_2, 1), dots, (2, e_2, 6)$ with 14 edges. +- Chain links: vertex 1 has edges $e_1, e_2$, so chain link $(1, e_1, 6) - (1, e_2, 1)$. Vertices 0 and 2 each have degree 1, so no chain links for them. +- Selector connections: $a_1$ connects to $(v, e_(v[1]), 1)$ and $(v, e_(v[deg(v)]), 6)$ for each $v in {0, 1, 2}$. + - $v = 0$: $a_1 - (0, e_1, 1)$ and $a_1 - (0, e_1, 6)$. + - $v = 1$: $a_1 - (1, e_1, 1)$ and $a_1 - (1, e_2, 6)$. + - $v = 2$: $a_1 - (2, e_2, 1)$ and $a_1 - (2, e_2, 6)$. + +Total: $|V'| = 1 + 24 = 25$ vertices. The Hamiltonian circuit for $C = {1}$: +$a_1 -> (1, e_1, 1) -> (0, e_1, 1) -> (0, e_1, 2) -> dots -> (0, e_1, 6)$ +$-> (1, e_1, 4) -> (1, e_1, 5) -> (1, e_1, 6) -> (1, e_2, 1)$ +$-> (2, e_2, 1) -> (2, e_2, 2) -> dots -> (2, e_2, 6)$ +$-> (1, e_2, 4) -> (1, e_2, 5) -> (1, e_2, 6) -> a_1$. + +In widget $e_1$: Pattern 1-only (vertex 1 covers, traverses all 12 vertices). +In widget $e_2$: Pattern 1-only (vertex 1 covers, traverses all 12 vertices). +All 25 vertices visited exactly once. $checkmark$ + +*Infeasible example (NO instance).* +Consider the triangle graph $K_3$ on vertices ${0, 1, 2}$ with edges +$E = {{0,1}, {0,2}, {1,2}}$, so $n = 3$, $m = 3$, and $K = 1$. + +The minimum vertex cover of $K_3$ has size 2 (any single vertex leaves one +edge uncovered). Since $K = 1 < 2$, there is no vertex cover of size 1. + +The constructed graph $G'$ has $|V'| = 1 + 36 = 37$ vertices. Since no +vertex cover of size 1 exists, the reduction guarantees that $G'$ has no +Hamiltonian circuit: a single selector can traverse the chain of only one +vertex, which covers at most 2 of the 3 edges, leaving one widget that +cannot be fully traversed. $checkmark$ diff --git a/docs/paper/verify-reductions/verify_vc_hc.py b/docs/paper/verify-reductions/verify_vc_hc.py new file mode 100644 index 00000000..ad1fed6f --- /dev/null +++ b/docs/paper/verify-reductions/verify_vc_hc.py @@ -0,0 +1,461 @@ +#!/usr/bin/env python3 +"""§1.1 MinimumVertexCover → HamiltonianCircuit (#198): exhaustive + structural verification. + +Garey & Johnson Theorem 3.4 gadget reduction. HC is NP-hard to check, so we use +a backtracking solver with pruning and limit to small graphs (n ≤ 4). +""" +import itertools +import sys +from sympy import symbols, simplify + +passed = failed = 0 + + +def check(condition, msg=""): + global passed, failed + if condition: + passed += 1 + else: + failed += 1 + print(f" FAIL: {msg}") + + +# ── Graph utilities ────────────────────────────────────────────────────── + + +def all_simple_graphs(n): + """Generate all non-isomorphic simple graphs on n labeled vertices. + Actually generates ALL labeled simple graphs (including isomorphic ones). + """ + vertices = list(range(n)) + possible_edges = list(itertools.combinations(vertices, 2)) + for r in range(len(possible_edges) + 1): + for edge_combo in itertools.combinations(possible_edges, r): + yield vertices, list(edge_combo) + + +def adjacency(n_vertices, edges): + """Build adjacency list from edge list.""" + adj = {v: set() for v in range(n_vertices)} + for u, v in edges: + adj[u].add(v) + adj[v].add(u) + return adj + + +def has_vertex_cover(n, edges, K): + """Brute force: does G have a vertex cover of size ≤ K?""" + vertices = list(range(n)) + for size in range(K + 1): + for cover in itertools.combinations(vertices, size): + cover_set = set(cover) + if all(u in cover_set or v in cover_set for u, v in edges): + return True + return False + + +def find_vertex_cover(n, edges, K): + """Find a vertex cover of size ≤ K, or None.""" + vertices = list(range(n)) + for size in range(K + 1): + for cover in itertools.combinations(vertices, size): + cover_set = set(cover) + if all(u in cover_set or v in cover_set for u, v in edges): + return list(cover) + return None + + +def has_hamiltonian_circuit(n_vertices, adj, timeout=500000): + """Backtracking HC solver with pruning. Returns True/False.""" + if n_vertices == 0: + return False + if n_vertices == 1: + return False # need at least a cycle + + # Check basic necessary conditions + for v in range(n_vertices): + if len(adj.get(v, set())) < 2: + return False # HC needs degree ≥ 2 + + start = 0 + path = [start] + visited = {start} + count = [0] + + def backtrack(): + count[0] += 1 + if count[0] > timeout: + return None # timeout + + if len(path) == n_vertices: + # Check if we can return to start + return start in adj.get(path[-1], set()) + + current = path[-1] + for neighbor in sorted(adj.get(current, set())): + if neighbor not in visited: + # Pruning: if adding this vertex would isolate an unvisited vertex + path.append(neighbor) + visited.add(neighbor) + result = backtrack() + if result is True: + return True + if result is None: + return None # propagate timeout + visited.remove(neighbor) + path.pop() + + return False + + result = backtrack() + if result is None: + return None # timeout + return result + + +# ── Reduction implementation ────────────────────────────────────────────── + + +def reduce(n, edges, K): + """Reduce VertexCover(G, K) to HamiltonianCircuit(G'). + + Returns: + (num_vertices, adj, vertex_names): the constructed graph G' + vertex_names maps index -> human-readable name + """ + # Order edges incident to each vertex + adj_source = adjacency(n, edges) + incident = {} # v -> ordered list of edges involving v + for v in range(n): + incident[v] = [] + for idx, (u, v) in enumerate(edges): + incident[u].append(idx) + incident[v].append(idx) + + # Assign vertex indices in G' + # Selectors: a_0, ..., a_{K-1} get indices 0..K-1 + # Widget vertices: for edge idx e = (u,v), vertex (endpoint, e, pos) + # where endpoint is u or v, pos is 1..6 + vertex_map = {} # (type, ...) -> index + vertex_names = {} + idx = 0 + + # Selectors + for j in range(K): + vertex_map[('sel', j)] = idx + vertex_names[idx] = f'a_{j}' + idx += 1 + + # Widget vertices + for e_idx, (u, v) in enumerate(edges): + for endpoint in [u, v]: + for pos in range(1, 7): + key = ('w', endpoint, e_idx, pos) + vertex_map[key] = idx + vertex_names[idx] = f'({endpoint},e{e_idx},{pos})' + idx += 1 + + num_vertices = idx + adj_target = {v: set() for v in range(num_vertices)} + + def add_edge(a, b): + adj_target[a].add(b) + adj_target[b].add(a) + + # Widget internal edges (14 per widget) + for e_idx, (u, v) in enumerate(edges): + # Horizontal chains + for endpoint in [u, v]: + for pos in range(1, 6): + a = vertex_map[('w', endpoint, e_idx, pos)] + b = vertex_map[('w', endpoint, e_idx, pos + 1)] + add_edge(a, b) + + # Cross edges + add_edge(vertex_map[('w', u, e_idx, 3)], vertex_map[('w', v, e_idx, 1)]) + add_edge(vertex_map[('w', v, e_idx, 3)], vertex_map[('w', u, e_idx, 1)]) + add_edge(vertex_map[('w', u, e_idx, 6)], vertex_map[('w', v, e_idx, 4)]) + add_edge(vertex_map[('w', v, e_idx, 6)], vertex_map[('w', u, e_idx, 4)]) + + # Chain links + for v in range(n): + chain = incident[v] # ordered list of edge indices incident to v + for i in range(len(chain) - 1): + e_curr = chain[i] + e_next = chain[i + 1] + a = vertex_map[('w', v, e_curr, 6)] + b = vertex_map[('w', v, e_next, 1)] + add_edge(a, b) + + # Selector connections + for j in range(K): + sel = vertex_map[('sel', j)] + for v in range(n): + if len(incident[v]) == 0: + continue # isolated vertex, no chain + first_e = incident[v][0] + last_e = incident[v][-1] + a = vertex_map[('w', v, first_e, 1)] + b = vertex_map[('w', v, last_e, 6)] + add_edge(sel, a) + add_edge(sel, b) + + return num_vertices, adj_target, vertex_map, vertex_names, incident + + +def count_edges(adj): + """Count undirected edges from adjacency dict.""" + return sum(len(neighbors) for neighbors in adj.values()) // 2 + + +def main(): + # === Section 1: Symbolic checks (sympy) — MANDATORY === + print("=== Section 1: Symbolic overhead verification ===") + + n_sym, m_sym, K_sym = symbols("n m K", positive=True, integer=True) + + # num_vertices = 12m + K + v_expr = 12 * m_sym + K_sym + check(simplify(v_expr - (12 * m_sym + K_sym)) == 0, "|V'| = 12m + K") + + # Verify for small values + for m_val in range(1, 6): + for K_val in range(1, 5): + expected_v = 12 * m_val + K_val + check(v_expr.subs({m_sym: m_val, K_sym: K_val}) == expected_v, + f"|V'|({m_val},{K_val}) = {expected_v}") + + # Widget has exactly 14 edges + check(10 + 4 == 14, "widget: 10 chain + 4 cross = 14 edges") + + print(f" Section 1: {passed} passed, {failed} failed") + + # === Section 2: Exhaustive forward + backward — MANDATORY === + print("\n=== Section 2: Exhaustive forward + backward ===") + sec2_start = passed + + # Test all graphs with n ≤ 4 vertices (skip n ≤ 1 as trivial) + for n in range(2, 5): + num_tested = 0 + for vertices, edges in all_simple_graphs(n): + if len(edges) == 0: + continue # no edges → trivial, skip + + # Count non-isolated vertices (those with degree ≥ 1) + non_isolated = sum(1 for v in range(n) if any(u == v or w == v for u, w in edges)) + for K in range(1, non_isolated + 1): + source_feasible = has_vertex_cover(n, edges, K) + nv, adj_t, vmap, vnames, inc = reduce(n, edges, K) + + # Check vertex count + check(nv == 12 * len(edges) + K, + f"n={n},m={len(edges)},K={K}: |V'|={nv}, expected {12*len(edges)+K}") + + # HC check with timeout + hc_result = has_hamiltonian_circuit(nv, adj_t, timeout=1000000) + + if hc_result is None: + # Timeout — skip this instance + continue + + check(source_feasible == hc_result, + f"n={n},m={len(edges)},K={K}: VC={source_feasible}, HC={hc_result}") + num_tested += 1 + + print(f" n={n}: tested {num_tested} instances") + + print(f" Section 2: {passed - sec2_start} new checks") + + # === Section 3: Solution extraction — MANDATORY === + print("\n=== Section 3: Solution extraction ===") + sec3_start = passed + + for n in range(2, 5): + for vertices, edges in all_simple_graphs(n): + if len(edges) == 0: + continue + for K in range(1, n + 1): + cover = find_vertex_cover(n, edges, K) + if cover is None: + continue + + # Verify the cover is valid + cover_set = set(cover) + check(all(u in cover_set or v in cover_set for u, v in edges), + f"extracted cover {cover} covers all edges") + + check(len(cover) <= K, + f"extracted cover size {len(cover)} ≤ K={K}") + + print(f" Section 3: {passed - sec3_start} new checks") + + # === Section 4: Overhead formula — MANDATORY === + print("\n=== Section 4: Overhead formula verification ===") + sec4_start = passed + + for n in range(2, 5): + for vertices, edges in all_simple_graphs(n): + if len(edges) == 0: + continue + m = len(edges) + for K in range(1, min(n + 1, 4)): + nv, adj_t, vmap, vnames, inc = reduce(n, edges, K) + + # Vertex count + check(nv == 12 * m + K, + f"overhead V: {nv} vs 12*{m}+{K}={12*m+K}") + + # Edge count + num_e = count_edges(adj_t) + widget_edges = 14 * m + chain_edges = sum(max(0, len(inc[v]) - 1) for v in range(n)) + non_isolated = sum(1 for v in range(n) if len(inc[v]) > 0) + sel_edges = 2 * non_isolated * K + expected_edges = widget_edges + chain_edges + sel_edges + + check(num_e == expected_edges, + f"overhead E: {num_e} vs {expected_edges} " + f"(14*{m} + {chain_edges} + 2*{non_isolated}*{K})") + + print(f" Section 4: {passed - sec4_start} new checks") + + # === Section 5: Structural properties — MANDATORY === + print("\n=== Section 5: Structural properties ===") + sec5_start = passed + + for n in range(2, 5): + for vertices, edges in all_simple_graphs(n): + if len(edges) == 0: + continue + m = len(edges) + K = min(n, 2) + nv, adj_t, vmap, vnames, inc = reduce(n, edges, K) + + # 1. Widget internal structure: exactly 14 edges per widget + for e_idx in range(m): + u, v = edges[e_idx] + widget_verts = set() + for ep in [u, v]: + for pos in range(1, 7): + widget_verts.add(vmap[('w', ep, e_idx, pos)]) + + # Count edges within this widget + widget_edge_count = 0 + for wv in widget_verts: + for nb in adj_t[wv]: + if nb in widget_verts and wv < nb: + widget_edge_count += 1 + + check(widget_edge_count == 14, + f"widget e{e_idx}: {widget_edge_count} internal edges, expected 14") + + # 2. Widget boundary vertices have correct degrees + for e_idx in range(m): + u, v = edges[e_idx] + # Boundary vertices: (u,e,1), (v,e,1), (u,e,6), (v,e,6) + for ep in [u, v]: + for pos in [1, 6]: + bv = vmap[('w', ep, e_idx, pos)] + # Internal degree from widget: pos 1 has chain(1-2) + possibly cross + # External degree: chain links + selector connections + # Just check it has degree ≥ 2 + check(len(adj_t[bv]) >= 2, + f"boundary ({ep},e{e_idx},{pos}) degree={len(adj_t[bv])} ≥ 2") + + # 3. Interior widget vertices (pos 2,3,4,5) have no external edges + for e_idx in range(m): + u, v = edges[e_idx] + widget_verts = set() + for ep in [u, v]: + for pos in range(1, 7): + widget_verts.add(vmap[('w', ep, e_idx, pos)]) + + for ep in [u, v]: + for pos in [2, 3, 4, 5]: + iv = vmap[('w', ep, e_idx, pos)] + external = [nb for nb in adj_t[iv] if nb not in widget_verts] + check(len(external) == 0, + f"interior ({ep},e{e_idx},{pos}) has {len(external)} external edges") + + # 4. Cross edges at correct positions + for e_idx in range(m): + u, v = edges[e_idx] + # (u,e,3) -- (v,e,1) + check(vmap[('w', v, e_idx, 1)] in adj_t[vmap[('w', u, e_idx, 3)]], + f"cross edge (u,e{e_idx},3)-(v,e{e_idx},1)") + # (v,e,3) -- (u,e,1) + check(vmap[('w', u, e_idx, 1)] in adj_t[vmap[('w', v, e_idx, 3)]], + f"cross edge (v,e{e_idx},3)-(u,e{e_idx},1)") + # (u,e,6) -- (v,e,4) + check(vmap[('w', v, e_idx, 4)] in adj_t[vmap[('w', u, e_idx, 6)]], + f"cross edge (u,e{e_idx},6)-(v,e{e_idx},4)") + # (v,e,6) -- (u,e,4) + check(vmap[('w', u, e_idx, 4)] in adj_t[vmap[('w', v, e_idx, 6)]], + f"cross edge (v,e{e_idx},6)-(u,e{e_idx},4)") + + # 5. Selector vertices connect to all vertex chain starts/ends + for j in range(K): + sel = vmap[('sel', j)] + for v_src in range(n): + if len(inc[v_src]) == 0: + continue + first_e = inc[v_src][0] + last_e = inc[v_src][-1] + start_v = vmap[('w', v_src, first_e, 1)] + end_v = vmap[('w', v_src, last_e, 6)] + check(start_v in adj_t[sel], + f"selector a_{j} -> chain start of v{v_src}") + check(end_v in adj_t[sel], + f"selector a_{j} -> chain end of v{v_src}") + + print(f" Section 5: {passed - sec5_start} new checks") + + # === Section 6: YES example from Typst — MANDATORY === + print("\n=== Section 6: YES example verification ===") + sec6_start = passed + + # P3: vertices {0,1,2}, edges {(0,1), (1,2)}, K=1 + # VC of size 1: {1} + yes_n, yes_edges, yes_K = 3, [(0, 1), (1, 2)], 1 + + check(has_vertex_cover(yes_n, yes_edges, yes_K), + "YES: P3 has vertex cover of size 1") + + nv, adj_t, vmap, vnames, inc = reduce(yes_n, yes_edges, yes_K) + check(nv == 25, f"YES: |V'| = {nv}, expected 25") + + hc = has_hamiltonian_circuit(nv, adj_t, timeout=5000000) + check(hc is True, f"YES: G' has Hamiltonian circuit = {hc}") + + # Verify cover = {1} + cover = find_vertex_cover(yes_n, yes_edges, yes_K) + check(set(cover) == {1}, f"YES: cover = {cover}, expected {{1}}") + + print(f" Section 6: {passed - sec6_start} new checks") + + # === Section 7: NO example from Typst — MANDATORY === + print("\n=== Section 7: NO example verification ===") + sec7_start = passed + + # K3: vertices {0,1,2}, edges {(0,1),(0,2),(1,2)}, K=1 + # Min vertex cover of K3 = 2, so K=1 is infeasible + no_n, no_edges, no_K = 3, [(0, 1), (0, 2), (1, 2)], 1 + + check(not has_vertex_cover(no_n, no_edges, no_K), + "NO: K3 has no vertex cover of size 1") + + nv_no, adj_no, vmap_no, vnames_no, inc_no = reduce(no_n, no_edges, no_K) + check(nv_no == 37, f"NO: |V'| = {nv_no}, expected 37") + + hc_no = has_hamiltonian_circuit(nv_no, adj_no, timeout=5000000) + check(hc_no is False, f"NO: G' has no Hamiltonian circuit = {hc_no}") + + print(f" Section 7: {passed - sec7_start} new checks") + + # ── Final report ── + print(f"\nMinimumVertexCover → HamiltonianCircuit: {passed} passed, {failed} failed") + return 1 if failed else 0 + + +if __name__ == "__main__": + sys.exit(main())